You're viewing the discuss.systems public feed.

Mariomario@don.tbully.me
Jul 29, 2026, 11:09 AM
@calx @0xabad1dea @shelldozer but they actually aren't magic :blobcat3c:
especially isabelle and rocq are actually somewhat easy to break down to their theoretic basics. they are very good tools to learn about proof theory.
💬 2🔄 0⭐ 0

Replies

Mans Rmansr@society.oftrolls.com
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.
💬 0🔄 2⭐ 7
Mariomario@don.tbully.me
Jul 29, 2026, 11:22 AM
@mansr @0xabad1dea @calx @shelldozer but that's out of scope of a theorem prover. that's on the person doing the formalization.
💬 1🔄 0⭐ 0
Crazazy @ my computer c:crazazy@tiny.tilde.website
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
💬 1🔄 0⭐ 3
Mariomario@don.tbully.me
Jul 29, 2026, 5:20 PM
@crazazy @0xabad1dea @calx @shelldozer @mansr
> limits
depends on the logic at hand. like first-order logic is complete and afaik solved within less than 200 characters of prolog
peano is incomplete, but here are other arithmetics that are complete like presburger that is complete.
💬 0🔄 0⭐ 0
calx u-latorcalx@infosec.exchange
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
💬 0🔄 0⭐ 1