Jul 29, 2026, 11:04 AM@mario @0xabad1dea @shelldozer not to say, they aren't magic, like i love theorem provers, and they are in a way very magical pieces of software humans have come up with
all this means is they shouldn't become the single source of truth
Jul 29, 2026, 11:17 AM@mario @0xabad1dea @calx @shelldozer Even with a flawless theorem prover, it is possible that what was proved isn't what you think it is because you made a mistake when formalising the theorem.
Jul 29, 2026, 5:15 PM@mario @0xabad1dea @calx @shelldozer @mansr if the person in question is formalizing a theorem prover, then that's definitely in the scope of problems.
Also you run into some gödel-esque problems when trying to fully prove the consistency of a theorem prover, within the theorem prover itself, so there are probably _some_ limits
Jul 29, 2026, 11:19 AM@mario @0xabad1dea @shelldozer ooo, interesting
tho, i'll have to read about them and metarocq before i can comment