3 ms·

I'm kinda amazed that no one has been able to write a proof solving AI yet. While a human AI is a very daunting task in order to capture "humaness" and large pr

by mhomde 12y ago

I'm kinda amazed that no one has been able to write a proof solving AI yet. While a human AI is a very daunting task in order to capture "humaness" and large problem-set it would seem to me that an AI working solely as a domain expert within maths should be much more feasible. Shouldn't you be able to build a database of all current proofs and have a computer be able to cross-reference and extrapolate from that? Sure it would be far from trivial but it seems doable. Mathematica/Wolfram for instance should be half way there. Here's the golden chance for a programmer to win x amount of Nobel prizes! :)

DMac87 12y ago
This is an area of research: http://en.wikipedia.org/wiki/Automated_theorem_proving http://en.wikipedia.org/wiki/Automated_theorem_proving
TTPrograms 12y ago
Automated proof checking software has been around for a while, and they don't really require any capacity I'd describe as 'AI' as they simply verify logic: https://en.wikipedia.org/wiki/Automated_proof_checking https://en.wikipedia.org/wiki/Automated_proof_checking The trouble is that writing a proof in a format amenable to this verification is harder and much more tedious than writing it for a paper
- mhomde 12y ago
  yes, that's why I think something different than Automated proof checking for solving advanced theorems, you need to have an AI that can take "creative leaps" and break down proofs down to something humans can understand, and not just verify existing rules
- deepsun 12y ago
  Some time ago I started designing a system that would convert between automated checkers syntax and some simplified human-readable English. But failed, once realized the problem is bigger than me. Here I just want to encourage anyone who thinks he's a good programmer to develop such a system. It would be extremely useful for education as well: students would get a tool that explains complex proofs, and professors would give assignments to put a theorem into the system (if student is able to enter the theorem into the system, then he/she definitely understands it up to the very foundations). The main problem to solve is good UX, not the math. They who manage to make the system, the new verified Wikipedia for Math, would have their names inscribed for eternity, because Math is eternal.
desdiv 12y ago
https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Automated_theorem_proving
temuze 12y ago
You mean x amount of Fields medals. There is no Nobel for math. Also, this is a lot harder than you think. "Extrapolating" from a learning set is relatively easy to do for statistical problems and prediction, but proofs are hard.
- mhomde 12y ago
  Ah sorry that's right, I always forget, maybe one in Economics then :)
tsomctl 12y ago
There are computer generated proofs. They are also completely unreadable, much less understandable, by humans. In reality, most of mathematics is based on set theory, which makes it hard for computers to reason about proofs. There is currently an effort to rebase mathematics on type theory, which would allow computers to verify and create proofs much more easily. However, basically all of mathematics has to be reproved using this new foundation. To give an example, group theory as taught in undergraduate classes depends completely on sets. A group itself is a set with additional properties. Subgroups are defined in terms of set intersection and union. Type theory is still in its infancy, and this stuff is still being figured out. In terms of Mathematica, it doesn't know jack shit about complicated math theorems. Can it tell you if a group is solvable?
- mhomde 12y ago
  Yeah, classifying math aspects and creating relations between different proofs is probably one of the thornier issues I'd guess. It does feel however that mathematics is a domain where an AI should be able to train itself in some way
- sukilot 12y ago
  Why are types easier than sets? They are both computable.

by mhomde 12y ago

DMac87 12y ago

This is an area of research: http://en.wikipedia.org/wiki/Automated_theorem_proving http://en.wikipedia.org/wiki/Automated_theorem_proving

TTPrograms 12y ago

Automated proof checking software has been around for a while, and they don't really require any capacity I'd describe as 'AI' as they simply verify logic: https://en.wikipedia.org/wiki/Automated_proof_checking https://en.wikipedia.org/wiki/Automated_proof_checking The trouble is that writing a proof in a format amenable to this verification is harder and much more tedious than writing it for a paper

mhomde 12y ago
yes, that's why I think something different than Automated proof checking for solving advanced theorems, you need to have an AI that can take "creative leaps" and break down proofs down to something humans can understand, and not just verify existing rules
deepsun 12y ago
Some time ago I started designing a system that would convert between automated checkers syntax and some simplified human-readable English. But failed, once realized the problem is bigger than me. Here I just want to encourage anyone who thinks he's a good programmer to develop such a system. It would be extremely useful for education as well: students would get a tool that explains complex proofs, and professors would give assignments to put a theorem into the system (if student is able to enter the theorem into the system, then he/she definitely understands it up to the very foundations). The main problem to solve is good UX, not the math. They who manage to make the system, the new verified Wikipedia for Math, would have their names inscribed for eternity, because Math is eternal.

desdiv 12y ago

https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Automated_theorem_proving

temuze 12y ago

You mean x amount of Fields medals. There is no Nobel for math. Also, this is a lot harder than you think. "Extrapolating" from a learning set is relatively easy to do for statistical problems and prediction, but proofs are hard.

mhomde 12y ago
Ah sorry that's right, I always forget, maybe one in Economics then :)

tsomctl 12y ago

There are computer generated proofs. They are also completely unreadable, much less understandable, by humans. In reality, most of mathematics is based on set theory, which makes it hard for computers to reason about proofs. There is currently an effort to rebase mathematics on type theory, which would allow computers to verify and create proofs much more easily. However, basically all of mathematics has to be reproved using this new foundation. To give an example, group theory as taught in undergraduate classes depends completely on sets. A group itself is a set with additional properties. Subgroups are defined in terms of set intersection and union. Type theory is still in its infancy, and this stuff is still being figured out. In terms of Mathematica, it doesn't know jack shit about complicated math theorems. Can it tell you if a group is solvable?

mhomde 12y ago
Yeah, classifying math aspects and creating relations between different proofs is probably one of the thornier issues I'd guess. It does feel however that mathematics is a domain where an AI should be able to train itself in some way
sukilot 12y ago
Why are types easier than sets? They are both computable.