Formalization and autoformalization

Leads: Scott Armstrong and Julia Kempe

Formalization means writing mathematics in a language that a computer can check line by line, using proof assistants such as Lean. Autoformalization means using AI to translate ordinary mathematical writing into that form.

We view formalization as the bridge that turns a large but static corpus of natural-language mathematics into a dynamic, extendable dataset, one that provides a verifiable training signal to the core. A proof that a computer has checked is a far stronger signal than a proof that only looks correct.

The area has three aims:

• Data for the core. Scaling autoformalization while keeping it faithful, so that a formal statement says what the original mathematics meant, and not something easier.
• Checking results. Providing independent, machine-checked verification of results obtained with AI in our pure mathematics work, and supporting the proof audits of our AI safety area.
• Beyond pure mathematics. Formalization extends naturally to applied mathematics, statistics and computational science. With our applied mathematics area we share the question of how to certify a computation: for example, an approximation together with a machine-checkable bound on its error.