The set.mm repo has a small set of Wiki pages. I've been putting notes about automated proving, especially AI/ML, here: https://github.com/metamath/set.mm/wiki/Automated-proving
I hope to someday work on AI/ML for creating Metamath proofs, but I haven't had a chance to do it. I encourage anyone interested to give it a try, I think it's *extremely* promising. --- David A. Wheeler > On Aug 19, 2023, at 8:32 PM, Amaury Hayat <[email protected]> wrote: > > Hi Marcel, > > There were actually several papers based on Transformers for Metamath. You > can probably check these two and the reference therein and it will give you a > good idea of what was done and what can be achieved (up to last year) :) > > https://arxiv.org/abs/2009.03393 > > https://arxiv.org/abs/2205.11491 > > For transformers learning more or less complicated specific maths notions > (ODE, stability of ODEs, equilibrium in graphs, linear algebra, etc.) you can > check for instance https://arxiv.org/abs/1912.01412 (learning to solve ODEs), > https://arxiv.org/abs/2006.06462 (learning to predict advance properties such > as stability, controllability, etc.), https://arxiv.org/abs/2112.03588 > (learning to find equilibrium in graphs), https://arxiv.org/abs/2112.01898 > (learning linear algebra). There are probably many other references but these > can give you a good start and their models and dataset are public. > > Best, > > > Le dim. 20 août 2023 à 06:30, 'Marcel Richter' via Metamath > <[email protected]> a écrit : > I had a lot of fun training transformers on some toy data, and now i am > thinking what to do next. I was surprised how fast even small transformers > lern long multiplication. > > Anyone know if someone trained a GTP on set.mm yet. > > set.mm is only ~40mb, i guess that is not enough to avoid overfitting really > fast. Anyone produced some procedural generated metamath code? > > I belive a well trained model could be of great help as some kind of > methamath copilote. > > Have a nice day :D > > -- > 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/1fe3d510-bd01-4097-8d04-6d4baac1f696n%40googlegroups.com. > > -- > 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/CAP92Bfkp3sWACxYbBnK%2Bz9Ah%3DOt4fw8cvewU2VnJKgSr99STeQ%40mail.gmail.com. -- 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/ACE9F6A9-30FC-43E0-8CDD-8D6926F94A5D%40dwheeler.com.
