Computers can solve math problems and prove theorems; this remains a significant subfield of Computer Science with lots of industrial use cases. However, pure machine learning based approaches toward these problems remain subpar.
> Even mathematical objects are approximated up to an approximation error in a computer (like a differentiable manifold or a real number).
Only because it caught on (and in the case of non-computationally-intensive applications, for purely historical reasons). For example, Mathematica has Reals and even functionality for Reals that is literally impossible to implement for integers [1,2]. There are also precise characterizations of objects in differential geometry [3]. You could imagine applying LLMs to these types of programs a la Copilot, but when you do this you will find yourself agreeing with Paul Houle's observation that math is harder to fake than eg art, language, or even glue code for web apps.
[1] https://reference.wolfram.com/language/ref/Reduce.html
[2] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
But the specification of the problem must be done by a human, translating to a formalized system that the software can understand. And if there's a problem in the formal specification, it's mostly up to the human to notice and fix; the computer will happily output garbage or crash or enter an infinite loop.
So it seems this translation, going from an exploration of the problem statement, usually in ambiguous terms, to a formal specification, and the awareness to possibly detect whether the answers make sense and the specs were right, is uniquely human.
https://en.wikipedia.org/wiki/Automated_theorem_proving
you just don't hear about it much because the technology is not so fashionable today. Also it is more clear what the limits are, I mean, Turing, Godel, Tarski and all of those apply to neural networks as well any other formal system but people mostly forget it.
Knuth wrote a really fun volume of The Art of Computer Programming about advances in SAT solvers which are the foundation for theorem provers
https://www.amazon.com/Art-Computer-Programming-Fascicle-Sat...
Everybody is aware that neural network techniques have improved drastically in performance, it's much more obscure that the toolbox of symbolic A.I. has improved greatly. Back in the 1980s production rules engines struggled to handle 10,000 rules, now Drools can handle 1,000,000+ rules with no problems.
It doesn't seem like there has been much progress for anything but FOL?
SMT solvers have gotten quite good over the past couple decades, there are tons of domain-specific tools (eg in software and hardware verification), tons of niche applied decidable or semi-decidable theories (eg various modal and description logics), a lot of progress on the proof assistant ("non-fully-automated theorem proving") paradigm, and so on.
It's not hard to add some extensions to logic for a particular application but a very hard problem to develop a general purpose extended logic.
I look at the logic-adjacent production rules systems which never really standardized some of the commonly necessary things such as agendas, priorities, defaults, etc.
I think sharemywin is probably on to something. It's going to be really hard for an AI to prove that e.g. x>0 && x+y <= 1 && y>1 is unsatisfiable, but it's trivial for an SMT solver. On the other hand it probably isn't that much of a leap to make an AI that can feed that problem into an SMT solver.
https://www.wolframalpha.com/calculators/integral-calculator...