Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: Crossposting invitation to AI maths study participation


Albert Jiang (Apr 12 2023 at 10:32):

https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Invitation.20to.20participate.20in.20AI.20maths.20assistant.20study

Fabian Glöckle (Apr 12 2023 at 11:30):

I consider this a very useful project: We have had lots of discussion on the LLM paradigm for mathematics on this channel recently to which this study would add reliable data. Also, it may be a proof of concept for how to overcome the GPT paradigm and ground LLMs in more than just next word prediction tasks for proofs.

Filippo A. E. Nuccio (Apr 15 2023 at 14:00):

I have tried participating in the study, but my browser systematically times out. Has someone been able to finish it?

Albert Jiang (Apr 15 2023 at 14:20):

Filippo A. E. Nuccio said:

I have tried participating in the study, but my browser systematically times out. Has someone been able to finish it?

Sorry to hear about your experience! We are using gradio hosting which communicates with an ssh connnection to us-west. It's highly possible that experiences differ because of that. We're trying to improve this experience. And thank you so much for your patience and time!

Filippo A. E. Nuccio (Apr 15 2023 at 16:02):

I will try again, perhaps tomorrow. For the time being, I still cannot go beyond the first page (the one I can access by clicking the very first LINK button).


Last updated: Dec 20 2023 at 11:08 UTC