Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: New Technologies in Mathematics Seminar at Harvard


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Jason Rute (Mar 05 2021 at 23:34):

As for my talk, the video is up on YouTube and the slides are here.

view this post on Zulip Jason Rute (Mar 05 2021 at 23:36):

We'd love for you to try out the tool. Join the discussion at #lean-gptf (or go straight to https://github.com/jesse-michael-han/lean-gptf for setup instructions.)


Last updated: May 09 2021 at 22:13 UTC