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.
Replies
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
- Mariomario@don.tbully.meJul 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.