Project summary

Large Reasoning Models are the future of mathematical AI since Large Language Models (LLMs) such as ChatGPT and Gemini hit a ceiling on how accurate and trustworthy they are mathematically. However. LRM's training data — formally verified proofs — barely exists beyond undergraduate level as relatively very few mathematicians can formalise/create them. Mathematical AI systems will increasingly automate high-stakes decisions in finance, science, and engineering. If LRMs are deployed in finance or infrastructure without high-quality formal training data, which we plan to produce, even rare mathematical errors could propagate into systemic failures leading to life and monetary loss. I am a Mathematics Master's student at the University of Bonn, one of the top Maths schools in the world, leading a programme through a non-profit that I direct to train graduate mathematicians as Lean formalisers, producing the first substantial corpus of graduate-level formal proofs. Our organisation has hosted several notable programs including research mentorship, research schools and outreach talks with the likes of Nobel laureates and Fields medalists. It has also partnered with several European institutions and is under the advisory of world-leading professors in Science and AI research. I'm seeking a 6-month personal stipend to focus on this full-time rather than splitting time with paid part-time work as a student. This project will be held in Bonn, in close proximity to the University of Bonn and Max Planck Institute Bonn, two top research institutions in mathematics globally.

What are this project's goals? How will you achieve them?

The goal is to address a specific bottleneck in mathematical AI: the near-total absence of graduate-level formally verified proofs as training data for Large Reasoning Models and human formalisers . This project pursues two concrete goals:

1. Train 15-20 graduate mathematics students as functional Lean 4 formalisers through a Directed Reading Programme to train students on Lean 4 from scratch (May 2026) and hands-on formalisation workshop to train them how to formalise graduate level mathematics with SOTA AI tools as support and top researchers hired as tutors/mentors, (June 2026), producing a corpus of graduate-level proofs contributed to Mathlib or another open academic repository (at least 30-50 results formalised)

2. Create a human formaliser experts pipeline, students who will continue to formalise graduate mathematics and contributing to the mathematical formalisation community

Both outputs directly feed the training data pipeline for mathematical AI systems that will increasingly automate high-stakes decisions in finance, science, and engineering.

How will this funding be used?

This is a personal stipend request only. The workshop programme itself is funded separately through institutional partners. This grant covers my personal subsistence (Bonn cost of living ~€800–1,000/month) for 6 months, enabling me to treat this as a full-time commitment rather than splitting focus with part-time paid work during the critical preparation and delivery window. This directly buys ~800–900 hours of focused work on curriculum, meetings, networking with researchers, attending conferences and dataset curation.

This grant funds my time only.

Who is on your team? What's your track record on similar projects?

I am a Mathematics Master's student at the University of Bonn. I am a Director of BMUCO (est. 2017), a science non-profit that has hosted lecture programmes featuring a Nobel Prize laureate in Physics and a Fields Medallist, co-hosted major international mathematics symposia with the Hausdorff Center for Mathematics (Bonn) and the Norwegian Academy of Science and Letters, and partnered with the London Institute for Mathematical Sciences. I have represented BMUCO at UN climate conferences (SB60, SB62) as a youth delegate. The project will be under the supervision of a notable and world-leading professor in Maths and AI research (details can be provided as asked) and we will hire top researchers in the team, which will be facilitated through our network here in Bonn and in London through our past programs and advisory network.

The programme is co-hosted with World Scientific Publishing and has active interest from industry.

What are the most likely causes and outcomes if this project fails?

The two most realistic failure modes are: (1) student engagement — formalising graduate mathematics in Lean 4 is genuinely difficult, and cohort attrition is possible if the learning curve proves too steep for participants without prior proof assistant experience; (2) timing — formal verification is growing rapidly in the mathematics community, but we may be slightly ahead of the curve in terms of how many graduate students are ready to commit to learning the tooling. Both risks are mitigated by the DRP structure, which provides guided mentorship before the workshop, and by the co-hosting support from World Scientific Publishing.

How much money have you raised in the last 12 months, and from where?

Zero personal income or grants. BMUCO has received small in-kind and event-level support from institutional co-hosts for past programmes, but no cash grants to the organisation or to me personally in the last 12 months. For this project, my org is actively raising funding, and pending final decision