Workshop

Formalizing Machine Learning Workshop

A gathering of researchers interested in (auto-)formalization of machine learning in Lean.

What?

Lean for Machine Learning and Machine Learning for Lean

Formalize Machine Learning in Lean

  • Mathlib, Lean's mathematical library, now has the prerequisites (in probability, linear algebra, and analysis) to formalize machine learning theory.

  • Building on this, we will explore how to start a large-scale formalization of machine learning in Lean.

Use AI autoformalization in a controlled way

  • The newest AI agents can help formalize mathematics: people have formalized whole books in Lean using AI agents.

  • However, nobody reuses the AI agents' output, and it's difficult to asses the quality of the code.

  • We explore ways to incorporate AI output into a human-certified library.

When and where?

Close to a NeurIPS location

Details

  • December 2026, before or after NeurIPS (to be determined)

  • In Lille, France. One hour by train from Paris, where NeurIPS is held.

  • Registration: to be announced. We will have a limited number of seats, so register early.

More information coming soon.

Sponsors

We are grateful for the support of the following organizations.