GRANT RECORD · RENAISSANCE PHILANTHROPY
Constraining LLMs for Theorem Proving
The goal of this project is to advance autoformalization—the task of translating informal mathematics into formal statements that can be automatically checked by state-of-the-art…
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
- Eleonora Giunchiglia · Sam Adam-Day · Joshua Ong · Mihaela Cătălina Stoian · Luca Andolfi
- 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.