Viewing profile — bckgrndrdtn

> These proof checkers all have bugs, every single one Please show me a proof of `False` in Lean.

It's a mixed bag. Some people don't use AI, for the usual reasons that people don't use AI. Others have used AI to write Lean programs. For example the 200K loc example mentioned i…

You are conflating: (i) accepting that a piece of code is a valid Lean proof (ii) merging a valid Lean proof into Mathlib. Valid Lean proofs need maintenance. Mathlib is a living b…

You would think that the people maintaining Mathlib are a subset of {understands type theory and how theorem provers work}... Yet they don't merge this stuff, for many different re…

All well and good, but we should also admit that under this criterion 95% of published math papers don't contain new ideas but are just filling in stuff that previous authors misse…

The future is now. See the article under discussion for some examples.

There's a lot to be said about that: https://lean-lang.org/doc/reference/latest/ValidatingProofs/ But let's assume Lean is perfect: - you have to trust your file system - you have …