Hacker News Reader

There is a language called lean which is popular among mathematicians. Here is an article: https://www.quantamagazine.org/building-the-mathematical-lib...

A more recent article as well: https://www.quantamagazine.org/lean-computer-program-confirm...

View on HN

My question was specifically referring to these huge 500 proofs that only a handful of people have even attempted to understand. What is the upper limit of what our current state-of-the-art proof assistants can handle?

The problem is not the limit of what proof checkers can handle - that probably goes beyond all known math. The problem is that long standing theories that 500 page proof is based on are not yet transcribed into formal language, so you'd need to do them first.

Reply on news.ycombinator.com