Meta shares research papers on AI helping solve open math problems

Meta says its AI models helped mathematicians solve six open research problems spanning a range of mathematical fields. The company is sharing the work as a set of six research papers.

The work comes from Meta’s Fundamental AI Research team, better known as FAIR, which has been bolstered by the company’s Superintelligence Labs. The effort is part of a multi-year push into mathematical reasoning, theorem proving, and formalization.

Formalization deserves a quick translation. It means rewriting human math into a strict language a computer can check line by line, so a proof either holds up or visibly breaks.

One of the most concrete results is an October 2, 2026 paper on solvable evolution algebras. In it, AI played a central role in disproving a conjecture put forward by researchers García-Martínez and Pérez-Rodríguez.

Shortly before that, on September 23, 2026, Meta released an arXiv preprint titled “Learning to Discover Interesting Mathematics.” The paper focuses on using post-trained large language models to generate theorems that are “interesting,” not merely true.

The textbook-eating robot

Earlier in the year, in May 2026, Meta launched AutoformBot. The system autoformalized 26 mathematics textbooks into Lean 4, a proof assistant used to verify mathematical arguments.

The output was a library of more than 45,000 declarations and hundreds of thousands of lines of verified code.

Researchers including Niket Patel and Amaury Hayat have been part of the team working on automating formalization and generating interesting theorems through machine learning.

Not Meta’s first lap around the track

Back in 2022, Meta AI was involved in solving 10 International Mathematical Olympiad problems using tools such as HyperTree Proof Search.

Meta is also far from alone. The broader field of AI-assisted mathematics surged in 2026, with papers arriving from multiple institutions, including OpenAI and Google DeepMind. Hundreds of AI-involved submissions have appeared on arXiv this year. A recurring feature across many of them is formal verification through systems like Lean, used to confirm that AI-generated results actually hold.

What this means

Meta is presenting these results as AI helping mathematicians, not replacing them, and the papers describe collaboration on problems that human researchers had already defined and pursued. The AI contributed to work like disproving the García-Martínez and Pérez-Rodríguez conjecture, but humans still chose the questions, interpreted the results, and wrote them up for peers to scrutinize.

Chatbot benchmarks can be gamed, disputed, or quietly retired. A disproved conjecture stays disproved, and a Lean-verified proof either compiles or it does not.