More (strong) evidence that agents make formal methods far more useful. The cost of creating that Lean proof has dropped dramatically.

Hopefully this helps mathematicians. It seems very clear to me that it will help software engineers apply formal methods to more of our software.