Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: Lean Together 2021 ML talks

Jason Rute (Jan 05 2021 at 00:53):

For those who don't follow the general channel, note there are a few talks tomorrow (Tuesday) early in the day on machine learning and theorem proving. You can find information about the conference (including links) at #Lean Together 2021 . If you can't make the talks, they will be recorded and put on the YouTube playlist soon after.

  • Stanislaus Polu OpenAI Metamath GPT-f
  • Jason Rute (me!) LeanStep: a dataset and environment for (interactive) neural theorem proving in Lean 3
    • 3pm CET (9am EST)
    • This is what it sounds like and it should be pretty cool! :smile:
    • Slides forthcoming
  • Koundinya Vajjha CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
    • 4:15 pm CET (10:15am EST)

Minchao Wu (Jan 05 2021 at 01:02):

Looking forward to it! How good is leanstep right now?

Jason Rute (Jan 05 2021 at 01:05):

The dataset? It's a pretty good one. :smirk:

Minchao Wu (Jan 05 2021 at 01:06):

No I mean the prover

Minchao Wu (Jan 05 2021 at 01:09):

Is there any preliminary results?

Jason Rute (Jan 05 2021 at 01:09):

Minchao Wu said:

No I mean the prover

I know. Tune in tomorrow. :)

Jason Rute (Jan 05 2021 at 16:24):

Here are the slides for my talk: https://docs.google.com/presentation/d/1poOu2gP9mSGAdAFvOupHvf4tpgD33jACQLJAVcphA1g/edit?usp=sharing

Last updated: Dec 20 2023 at 11:08 UTC