alt Hacker NewsI am not a mathematician but are most papers now accompanied by a lean proof?
Is there a central repository of lean proofs shared by mathematicians like an npm repository of JavaScript packages?
Does it all depend on a stupid is-odd package in the end?
Replies
danabramov • today at 5:23 PM
It's new but there is actually a registry now: https://palomar-registry.org/
UltraSane • today at 5:34 PM
LLMs have gotten good at creating Lean proofs so the are much more common but not universal. And they depend on https://github.com/leanprover-community/mathlib4
No, almost none (except for in certain fields, such as HoTT) have formalized proofs.