bckgrndrdtn

6 ms·

1. 1.▲
   by bckgrndrdtn 3mo ago

   > These proof checkers all have bugs, every single one Please show me a proof of `False` in Lean.
2. 2.▲
   by bckgrndrdtn 3mo ago

   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 in OP. But generally speaking, the quality isn
3. 3.▲
   by bckgrndrdtn 3mo ago

   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 blob of code. People care about how fast the proofs typecheck
4. 4.▲
   by bckgrndrdtn 3mo ago

   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 reasons, including that those 200K lines are free as in p
5. 5.▲
   by bckgrndrdtn 3mo ago

   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 missed.
6. 6.▲
   by bckgrndrdtn 3mo ago

   The future is now. See the article under discussion for some examples.
7. 7.▲
   by bckgrndrdtn 3mo ago

   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 to trust your