AI

135 views
Skip to first unread message

fl

unread,
Jan 15, 2020, 7:14:02 AM1/15/20
to Metamath

vvs

unread,
Jan 15, 2020, 8:16:42 AM1/15/20
to Metamath
I was very interested in FOMM 2020, but as there is no transcript I'm forced to look at slides and read some second hand impressions. In case someone missed it and as it's to some extent related to subject:

"Mario Carneiro talked about metamath 0. I wish I could say more about his work, but it is too foundational for me to understand it properly. All I know is that we had a proof of Dirichlet’s theorem on primes in an AP in metamath and then Mario pressed a button and we had one in Lean, and it had been written by a computer and was incomprehensible. Scary?"

That were Kevin Buzzard's impressions :)

BTW, in those slides the line was drawn between verification and synthesis. I think this is important too.

Olivier Binda

unread,
Jan 15, 2020, 8:28:57 AM1/15/20
to meta...@googlegroups.com
thanks for the link. I'm really interested in that.

Basically, the article says that they have a neural network (they hint at it's composition but don't give the model), 
They train it with with pairs of (problem, solution) written in a language analogous to metamath (trees for expression)
and then, they stop the training process and tipically make their trained system solve problems analogous to those it has been trained for.

Apparently, they used billions of pairs to train their model and get quite good results at integration (99.7%) and decent resultds at dsolving ifferential equations (80+ish %)

Having done the same 3 years ago, to train an android app to recognize Japanese characters, the approach is standard. 
What is important though is :
1) the model (not given)
2) the training set (not given either)

So, it basically confirms what we could guess : 
Neural network (humans) can be really good at different part of maths with a decent training.

It'll just be hard (but not impossible) to reproduce what they do, to incorporate it in some metamath tooling though... :/

Edit : nonetheless, this article gives some very invaluable information : 
If you write a tool that looks for a function g whose derivative is f. with 99.7% of accuraccy (and the speed of ml/it just takes some milliseconds to compute some multidimensionals number arrays),
Machine learning is the way to go. And if you do it the right way, you are going to build a very good tool, fast and accurate (state of the art). 
This is some really precious information.

Norman Megill

unread,
Jan 15, 2020, 11:40:30 AM1/15/20
to Metamath
More AI

"Calculemus!":  Leibniz believed calculation would be the key to settling all human disagreements.  A famous attempt was Godel's 1970 ontological argument, which was puzzled over and discussed by philosophers for decades, until 2013 when an AI-based theorem prover discovered an inconsistency that has been confirmed by a proof verifier (Isabelle I think). https://www.ijcai.org/Proceedings/16/Papers/137.pdf

An AI paper under review is https://openreview.net/pdf?id=BJxiqxSYPB that "advances the state of the art of automated theorem proving in Metamath."  I don't know who wrote it.

Norm


On Wednesday, January 15, 2020 at 7:14:02 AM UTC-5, fl wrote:

Jon P

unread,
Jan 15, 2020, 12:48:33 PM1/15/20
to Metamath
That paper is interesting, I was wondering a similar thing about whether it would be possible to generate training data for an mm prover by just making random substitutions. Looks like they have gone one better and trained the generator on human proofs to try and make it make more reasonable things.

I'm finding it a bit hard to interpret their results. Does table 3 mean their best result is proving 574/2720 of their test theorems? That would mean about 21% up from holophrasms 14%?

One thing I wonder about the future of theorem proving is would there be value in having a list of results which were desired to be formally proven but which are not yet? So basically a formalised version of a theorem with hypotheses and the theorem statement and no proof? For both AI and people one challenge is working out what statements are desired to be proven and then a second challenge is to prove them.

Mario Carneiro

unread,
Jan 15, 2020, 2:09:40 PM1/15/20
to metamath
On Wed, Jan 15, 2020 at 8:16 AM vvs <vvs...@gmail.com> wrote:
I was very interested in FOMM 2020, but as there is no transcript I'm forced to look at slides and read some second hand impressions.

All the talks were recorded and streamed, and they are set to appear on youtube shortly. I'll post a link when they come out.
 
In case someone missed it and as it's to some extent related to subject:

"Mario Carneiro talked about metamath 0. I wish I could say more about his work, but it is too foundational for me to understand it properly. All I know is that we had a proof of Dirichlet’s theorem on primes in an AP in metamath and then Mario pressed a button and we had one in Lean, and it had been written by a computer and was incomprehensible. Scary?"

That were Kevin Buzzard's impressions :)

I had to skip the demo due to time constraints (or time management issues), so it ended up looking mostly like a theoretical analysis of bootstrapping theorem provers rather than "Mario shows us a weird proof assistant" which was what I was actually going for. Oh well.

Mario

fl

unread,
Jan 16, 2020, 7:36:46 AM1/16/20
to Metamath

"Calculemus!":  Leibniz believed calculation would be the key to settling all human disagreements.


I will still be told that I am off topic, but Leibniz never said that all human problems would be settled by logic. 
On the contrary, he had a rather pessimistic philosophy (he was a Protestant): the world is the best of all possible worlds; 
that is to say, even if God is perfectly good, evil exists and will continue to exist because of the structure of reality that 
prevents God from doing better. It is true that he recommended an intensive use of formal logic in all sectors of human 
activity (philosophy and laws for example) but it was more like a way of not introducing more errors if they are avoidable. 
He gave the example of those trials where people were sentenced to death because of an error in the judge's reasoning. 
He also thought that formal logic allows people to understand each other better since there is no polysemy. His quarrels 
with Newton at the end of his life show that he may have gone a little too far.

-- 
FL

fl

unread,
Jan 16, 2020, 12:12:20 PM1/16/20
to Metamath

I will still be told that I am off topic, but Leibniz never said that all human problems would be settled by logic. 


I prefer to warn because if some people think, based on Leibniz, that we will remedy the ecological disaster with AI,
they are very much mistaken.

--
FL

vvs

unread,
Jan 16, 2020, 12:50:53 PM1/16/20
to Metamath
I will still be told that I am off topic, but Leibniz never said that all human problems would be settled by logic. 

This is an extreme view. I don't believe that anyone could view history or philosophy of mathematics, especially relevant to logic as "off-topic".
 
I prefer to warn because if some people think, based on Leibniz, that we will remedy the ecological disaster with AI,
they are very much mistaken.

They will be at least naive. And that's what making any such discussions outside of expert community useless at best or demagogy at worst. But of course people tend to complain about their grievances anyway. But what good will it make (except make them feel better)? Heck, it's impossible to get most programmers fix even their own bugs. Does somebody believes that a few strangers can affect world markets by just complaining? BTW, "contrary" to expectations Greta doesn't post her grievances on Facebook by herself, you know... I've told you, I'm cynical.

BTW, let's first define what AI should really mean. Is it some sentient thing (whatever that mean) or just a statistical trick? If the latter then I see that term just as a hype.

Mario Carneiro

unread,
Jan 18, 2020, 5:05:49 PM1/18/20
to metamath
On Wed, Jan 15, 2020 at 2:09 PM Mario Carneiro <di....@gmail.com> wrote:


On Wed, Jan 15, 2020 at 8:16 AM vvs <vvs...@gmail.com> wrote:
I was very interested in FOMM 2020, but as there is no transcript I'm forced to look at slides and read some second hand impressions.

All the talks were recorded and streamed, and they are set to appear on youtube shortly. I'll post a link when they come out.


OlivierBinda

unread,
Jan 19, 2020, 2:23:00 AM1/19/20
to meta...@googlegroups.com

Nice slides... (me salivates at MM0, wanna use it, wanna use it)

On my side, I have made some nice breakthroughs these past weeks
and I think that I am on track to disrupt what people think about how interactive theorem provers should look
(well, we shall see).

I just need a few more days to polish things further and I'll release a video of Mephistolus Milestone 6

Best regards,
Olivier

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuVkXKCHFP4VmEtqxcxftjaLym7wf84qzVRpgcR%2BnM%2BOw%40mail.gmail.com.

vvs

unread,
Jan 19, 2020, 9:12:15 AM1/19/20
to Metamath

Thanks.


The most interesting to me are MM0 and Lean4 (which got a few more tactics today, yay). Kevin Buzzard's talk looks nice too.

Unfortunately the slides are washed out in the video, so you will have to follow along here:


Yes, there is a warning already.

Jon P

unread,
Jan 19, 2020, 11:31:48 AM1/19/20
to Metamath
Hi Mario, that was a nice talk, your work is very interesting. 

Can I ask about classic search to produce metamath proofs? You say MM0 is a lot quicker and is not yet parallelised as that is not required at the moment. I find it a bit hard to work out the branching factor for an MM proof, I imagine it is quite high, however if you parallelised your system how many steps deep do you think you could get with a breadth first search? Even a search that could do 3 or 4 steps deep might be powerful for speeding up proving things. 

Anyway thanks it was interesting.
Reply all
Reply to author
Forward
0 new messages