6 ms·

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

• nerdponx 5y ago
  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?
  • lostmsu 5y ago
    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.