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

Princeton University, Princeton NJ

Investigators

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, integrated with preference alignment to ensure correctness and enable a self-improving system guided by symbolic proof signals. Together, these elements form a closed-loop system for scalable, trustworthy proof generation. Anticipated outcomes include new Hadamard matrix constructions, practical software for AI-assisted mathematics, and foundational advances in combining learning and logic for mathematical problem solving. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.