Automated mathematical reasoning.

  • 3 Replies
  • 5333 Views
*

infurl

  • Administrator
  • **********
  • Millennium Man
  • *
  • 1040
  • 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
  • ***********
  • Eve
  • *
  • 1468
    • contrast-zone
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.
There exist some rules interwoven within this world. As much as it is a blessing, so much it is a curse.

*

ivan.moony

  • Trusty Member
  • ***********
  • Eve
  • *
  • 1468
    • contrast-zone
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.
There exist some rules interwoven within this world. As much as it is a blessing, so much it is a curse.

*

ivan.moony

  • Trusty Member
  • ***********
  • Eve
  • *
  • 1468
    • contrast-zone
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.
There exist some rules interwoven within this world. As much as it is a blessing, so much it is a curse.

 


GTP-3 is bigoted!
by frankinstien (AI News )
January 20, 2021, 10:00:31 pm
White House Launches National AI Office
by MikeB (AI News )
January 15, 2021, 03:45:53 am
DALL-E text & image 2 image !!!!!
by LOCKSUIT (AI News )
January 06, 2021, 08:14:52 pm
Creating a VR sense of temperature
by frankinstien (AI News )
January 02, 2021, 09:19:51 am
Robots dancing better than us?
by 8pla.net (Robotics News)
December 31, 2020, 05:54:29 am
Bjarne Stroustrup (the creator of C++) talks about Machine Learning
by MikeB (AI News )
December 19, 2020, 12:26:31 pm
Wheels Are Better Than Feet for Legged Robots
by HS (Robotics News)
December 10, 2020, 07:51:29 pm
Getting a bot to smell!
by frankinstien (AI News )
December 09, 2020, 03:53:00 pm

Users Online

127 Guests, 0 Users

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

Articles