GRANT RECORD · RENAISSANCE PHILANTHROPY
Document-Level Autoformalization
The project will develop open-source tools to automate the formalization of mathematical documents, enabling algorithmic verification of research-level mathematics using the Lean proof assistant.…
Published amountAmount not published
No amount is inferred from fund totals or application caps.
Status semanticspublished award; amount and payment timing not published
Publication does not independently prove payment.
Award or decision dateNot published
The row exposes no award or decision date.
WHO AND WHAT
Parties and purpose.
- Recipient or team
- Antoine Bosselut · Viktor Kunčak
- Originating funder
- XTX Markets →
- Adviser or administrator
- Renaissance Philanthropy →
- Cause
- science-and-technology
- Intervention
- AI for mathematics research and infrastructure
- Geography
- Not published
- Focus areas
- AI for mathematics
- Listed funds
- AI for Math Fund
SOURCE TRAIL
Trace the claim.
Coverage note. RenPhil states that the first round contained 29 awards, but its current portfolio page exposes 28 named project records. This snapshot imports those 28 and records one unresolved coverage gap. Row-level award amounts and decision/payment dates are not published.