Mathematician Updates Lean Formalization Progress
Scott Armstrong details his 2026 workflow shift from impossible to practical.
Scott Armstrong posted an update on Lean auto-formalization in his own research workflow. He described the change in 2026 from impossible for his papers in March, to possible but too costly in time and tokens in May, to now practical in July. Jaume de Dios replied that auto formalization is really here and every mathematician should be updating their priors on it.
An update on Lean (auto)-formalization. Speaking about my own research workflow, in 2026, we have gone from: March: Lean formalization is not possible (for my papers). May: Lean formalization is possible... but way too costly in time and tokens to be practical most of the…
Reactions from ranked influencers
1 postThis is something every mathematician should be updating their priors on right now, auto formalization is really here!
An update on Lean (auto)-formalization. Speaking about my own research workflow, in 2026, we have gone from: March: Lean formalization is not possible (for my papers). May: Lean formalization is possible... but way too costly in time and tokens to be practical most of the…
