@davidlowryduda@mathstodon.xyz
2026-09-08 21:02 UTC
@slowcoding@social.vivaldi.net Largely their effectiveness. Automated theorem provers aren't very good at proving theorems and the field is instead dominated by what might be better called "automated theorem verifiers"
Replies (1)
-
@StephanSchulz@fosstodon.org 2026-09-09 07:00
@davidlowryduda@mathstodon.xyz @slowcoding@social.vivaldi.net Automated Theorem Provers are quite good at solving some kinds of problems. But they are not, in themselves, good at building deeply nested proofs, and coming up with new definitions and lemmas. They are also only now getting access to vast libraries of mathematics in their formalisms (autoformalization as a field largely grew out of ATP). Their successes are in limited fields (like loop theory or Tao's Equational Theories Project - ATPs can essentially solve that).