[infurl]

https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/

In the 1970s, the late mathematician Paul Cohen, the only person to ever win a Fields Medal for work in mathematical logic, reportedly made a sweeping prediction that continues to excite and irritate mathematicians — that “at some unspecified future time, mathematicians would be replaced by computers.” Cohen, legendary for his daring methods in set theory, predicted that all of mathematics could be automated, including the writing of proofs.

To accomplish this requires a combination of inductive and deductive reasoning. While advances continue to be made at a steady pace, and have been augmented more recently by machine learning techniques, we're not even close yet. For most mathematicians, the best available tool is still a pencil and paper.

[ivan.moony]

Hilbert had a great idea about this matter. Too bad it is not completely realizable. But it would be an awesome direction for science to go towards.

[ivan.moony]

In the article, it is described how theorem provers break into two categories: (1) automated theorem provers, and (2) proof verifiers. In another axis, less known, but maybe even more characteristic, there are theorem provers based on: (1) logic, and (2) lambda calculus. There are other foundations too, like Martin Löf's Type Theory, but the former two are the most popular.

However, (1) logic and (2) lambda calculus are shown being equal in Curry-Howard Correspondence thesis. Nevertheless, in current software appearance there is a clear polarization between the two concepts, yielding logic programming languages from (1) and functional programming from (2).

Maybe someone heard of Turing machines too, as a model for computation. Today's computer architecture is more similar to Turing machines than to lambda calculus, yet Turing himself, shortly after lambda calculus was introduced to him, concluded that TM and LC are equivalent model of computation. I failed to see this similarity, but if it's true, then (1) assembler/imperative programming is similar to (2) lambda calculus, which is in turn similar to (3) logic (by C-H correspondence). Yet, instead of one general, the three distinct paradigms still rock the world: (1) assembler/imperative programming, (2) functional programming, and (3) logic programming. There are other paradigms too, but they are less known.

And like this was not enough, artificial neural networks appeared as a new computational model, a favorite candidate to represent computations that we, humans, perform in our brains. But I believe the former three paradigms are indeed similar, or at least computationally equivalent, while ANN is that much complex that it may only represent an algorithm that can operate on any of the three paradigms.

[ivan.moony]

Here is some of my latest work in this field: e-log specification. This may not seem like a big deal, but it is to me. The most important achievement is easy mapping of functional programming expressions to logic programming expressions. To do this, I extended propositional logic by two simple concepts: (1) propositional sequences and (2) scoping expressions. That seems to be enough to reach Turing completeness.