2026-09-09 07:00 UTC
@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).
Replies (1)
-
@slowcoding@social.vivaldi.net 2026-09-09 21:11
@StephanSchulz@fosstodon.org @davidlowryduda@mathstodon.xyz ok, but is that an inherent problem with how these tools work? Have we ever tried to throw as much compute to them as we are doing with LLM (training+inference)? How would they scale? LLMs sound like clever random walks in the solution space whereas these tools sound like systematic explorations. Is there more to it fundamentally ?