Automated mathematical reasoning.

  • 3 Replies
  • 26528 Views
*

infurl

  • Administrator
  • ***********
  • Eve
  • *
  • 1365
  • Humans will disappoint you.
    • Home Page
Automated mathematical reasoning.
« on: August 31, 2020, 02:34:51 am »
https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/

Quote
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

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1723
    • mind-child
Re: Automated mathematical reasoning.
« Reply #1 on: August 31, 2020, 03:13:12 am »
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

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1723
    • mind-child
Re: Automated mathematical reasoning.
« Reply #2 on: September 02, 2020, 01:14:14 am »
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

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1723
    • mind-child
Re: Automated mathematical reasoning.
« Reply #3 on: September 02, 2020, 04:35:04 pm »
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.

 


OpenAI Speech-to-Speech Reasoning Demo
by ivan.moony (AI News )
March 28, 2024, 01:31:53 pm
Say good-bye to GPUs...
by MikeB (AI News )
March 23, 2024, 09:23:52 am
Google Bard report
by ivan.moony (AI News )
February 14, 2024, 04:42:23 pm
Elon Musk's xAI Grok Chatbot
by MikeB (AI News )
December 11, 2023, 06:26:33 am
Nvidia Hype
by 8pla.net (AI News )
December 06, 2023, 10:04:52 pm
How will the OpenAI CEO being Fired affect ChatGPT?
by 8pla.net (AI News )
December 06, 2023, 09:54:25 pm
Independent AI sovereignties
by WriterOfMinds (AI News )
November 08, 2023, 04:51:21 am
LLaMA2 Meta's chatbot released
by 8pla.net (AI News )
October 18, 2023, 11:41:21 pm

Users Online

314 Guests, 0 Users

Most Online Today: 396. Most Online Ever: 2369 (November 21, 2020, 04:08:13 pm)

Articles