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