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... :/ Le mercredi 15 janvier 2020 14:16:42 UTC+1, vvs a écrit : > > 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. > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ba4dbe39-da2c-4767-9445-719b16461d4e%40googlegroups.com.
