Hacker News Reader

Comment by mhomde | Hacker News Reader

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! :)

View on HN

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?

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

Why are types easier than sets? They are both computable.

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

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

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

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.

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.

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

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

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

Reply on news.ycombinator.com