Jason Rute (Mar 03 2021 at 13:11):
In general, the Harvard New Technologies in Mathematics Seminar is focusing this semester on topics related to interactive theorem proving and machine learning. There have already been recorded talks by Josef Urban, Christian Szegedy, and others.
Jason Rute (Mar 03 2021 at 13:16):
Today's talk is by me. In that talk, which is in 7 hours, at 3pm EST (UTC-5) on Zoom, I'm going to discuss our machine learned Lean
gptf tactic and the PACT method we use to train the current version. There will be a demo. Here is the abstract and Zoom link. I also think it will be recorded and put on YouTube. I think the best place to discuss this will be at the #lean-gptf stream (but we will be happy to field questions anywhere).
Jason Rute (Mar 05 2021 at 23:34):
Jason Rute (Mar 05 2021 at 23:36):
Last updated: May 09 2021 at 22:13 UTC