β-redex comments on Lies, Damned Lies, and Proofs: Formal Methods are not Slopless

β-redex 5 Jun 2026 20:05 UTC
1 point
0
I just noticed that there now is a Lean checking system that’s intended to be adversarially robust: https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-comparator

https://github.com/leanprover/comparator
- Max von Hippel 17 Jun 2026 18:49 UTC
  2 points
  0
  Parent
  Yes! I believe Axiom AI has been involved with this effort.