Mathematician Updates Lean Formalization Progress

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.