# Collaborative Research: AIMing: Towards the Hadamard Conjecture: A Unified Neurosymbolic Reasoning and Formal Verification Paradigm

> **NSF 01002526DB NSF RESEARCH & RELATED ACTIVIT** · Princeton University (NJ) · $250,000

## Abstract

This project aims to develop a new artificial intelligence system that works alongside mathematicians to tackle problems that have resisted solutions for nearly a century. Recent advances in large language models can generate creative insights and partial reasoning steps, but they often make mistakes and cannot guarantee correctness. In contrast, traditional tools for verifying mathematical proofs offer rigorous guarantees but are not well-suited for automatically navigating the vast search spaces involved in complex mathematical discovery. This research combines the strengths of both approaches: using AI to explore promising ideas and using formal logic to rigorously verify and refine them. As a high-impact test case, the team will focus on the Hadamard Conjecture, a longstanding open problem with applications in quantum error correction, communication systems, and coding theory. The project will also produce open-source tools, educational materials, and outreach programs to broaden participation in advanced mathematics and AI.

The research introduces a unified framework with three key components: (1) a self-evolving reasoning pipeline that uses synthetic data to guide exploration of promising matrix constructions; (2) chain-of-thought and curriculum learning to help AI decompose complex mathematical tasks into simpler subproblems, integrate partial solutions, and generalize from simpler to more difficult problems; and (3) formal verification tools, such as Lean, integrat

## Key facts

- **NSF award ID:** 2523385
- **Awardee organization:** Princeton University (NJ)
- **SAM.gov UEI:** NJ1YPQXQG7U5
- **PI:** Jason Lee
- **Primary program:** 01002526DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** Artificial Intelligence (AI), Machine Learning Theory
- **Estimated total:** $250,000
- **Funds obligated:** $250,000
- **Transaction type:** Standard Grant
- **Period:** 09/01/2025 → 09/30/2025

## Primary source

NSF Award Search: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2523385

## Citation

> US National Science Foundation, Award 2523385, Collaborative Research: AIMing: Towards the Hadamard Conjecture: A Unified Neurosymbolic Reasoning and Formal Verification Paradigm. Retrieved via AI Analytics 2026-06-07 from https://api.ai-analytics.org/grant/nsf/2523385. Licensed CC0.

---

*[NSF Awards dataset](/datasets/nsf-awards) · CC0 1.0*