Leo on "Proof Assistants in the Age of AI"

Stream: general

[Kim Morrison]

Just linking to a blog post Leo wrote today: https://leodemoura.github.io/blog/2026/02/18/proof-assistants-in-the-age-of-ai.html

[Wrenna Robson]

God Leo is so good.

[Wrenna Robson]

Like I don't mean to gush but I really intellectually respect him and I hope I get a chance to meet him one day and say thanks.

[Kevin Buzzard]

Yeah he's very wise, that's how we've got this far!

[Edward van de Meent]

Wrenna Robson said:

God Leo is so good.

is there an intentional lack of punctuation here?

[Johan Commelin]

The point of "Automation as Game Moves" made me think of the first three levers in https://steve-yegge.medium.com/software-survival-3-0-97a2a6255f7b

[Filippo A. E. Nuccio]

Beautiful text! I particularly like the sentence

When the definitions are clear and the tooling is helpful, mathematicians can engage with the formal library directly. When they are obscured by encoding overhead, the gap between informal and formal mathematics remains, no matter how many theorems are verified.