3 ms·
This is fascinating. If i had more time to get an articulate question i would, but I'm going to need to sit with this paper for a bit. Amazingly, I've been fo
by dtornabene 10y ago
This is fascinating. If i had more time to get an articulate question i would, but I'm going to need to sit with this paper for a bit. Amazingly, I've been fooling around on the edges of thereom proving for a bit now and had yet to hear of the Mizar corpus. Really, really fascinating stuff.
- aab0 10y agoYou should read https://intelligence.org/2013/12/21/josef-urban-on-machine-learning-and-automated-reasoning/ https://intelligence.org/2013/12/21/josef-urban-on-machine-l... and the citations! After that, you almost wonder why no one had applied NNs before.
- justifier 10y agohere is an example of the mizar corpus http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?decode=list+of+th+from+euclid_5&input=list+of+th+from+euclid_5 http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?deco... it was the first result at the time from: http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename=articles.author.mqt&argument=number+1 http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename...
- dtornabene 10y agothanks for the link, started and bookmarked. Lots to get on top of in that interview! There was a feeling reading the original paper of "why has no one done this yet" but I don't have the chops to ask that, yet.