3 ms·

I'm relieved that Lean4 doesn't seem to be some AI thing.

by opan 3y ago

sebzim4500 3y ago
There is a project to connect GPT-4 and lean, but I doubt they will make a lot of progress until they can finetune GPT-4. https://www.youtube.com/watch?v=CEwRMT0GpKo https://www.youtube.com/watch?v=CEwRMT0GpKo
zozbot234 3y ago
Automated reasoning is usually included in AI (Lean4 has tactics so it qualifies as such) but it's also quite different from the ML stuff that's the more usual kind of AI these days.
- rprenger 3y ago
  You can have both! LeanDojo: Theorem Proving with Retrieval-Augmented Language Models https://arxiv.org/abs/2306.15626 https://arxiv.org/abs/2306.15626 (shameless plug)
- alexvitkov 3y ago
  Things usually stop being considered as AI when they start working.
julianeon 3y ago
Now that you mention it, Tao did say he used ChatGPT to help teach himself Lean. https://x.com/8teapi/status/1713867160886599920?s=46&t=4jd61tn6MlpOFUFSrupxWg https://x.com/8teapi/status/1713867160886599920?s=46&t=4jd61...
- svat 3y ago
  Instead of a twitter post of screenshots of it, the direct link to Tao's Mathstodon is: https://mathstodon.xyz/@tao https://mathstodon.xyz/@tao He's been posting about it since Oct 9: https://mathstodon.xyz/@tao/111206761117553482 https://mathstodon.xyz/@tao/111206761117553482 > I have decided to finally get acquainted with the #Lean4 interactive proof system (using AI assistance as necessary to help me use it), as I now have a sample result (in the theory of inequalities of finitely many real variables) which I recently completed (and which will be on the arXiv shortly), which should hopefully be fairly straightforward to formalize. I plan to journal here my learning process, starting as someone who has not written a single line of Lean code before. There are several posts mentioning how GPT has been useful (though not always) at suggesting things, including one linking to this transcript with ChatGPT: https://chat.openai.com/share/857353ad-a05b-4f9e-bb10-55f15a2bd871 https://chat.openai.com/share/857353ad-a05b-4f9e-bb10-55f15a...

I'm relieved that Lean4 doesn't seem to be some AI thing.

by opan 3y ago

I'm relieved that Lean4 doesn't seem to be some AI thing.

There is a project to connect GPT-4 and lean, but I doubt they will make a lot of progress until they can finetune GPT-4. https://www.youtube.com/watch?v=CEwRMT0GpKo https://www.youtube.com/watch?v=CEwRMT0GpKo

zozbot234 3y ago

Automated reasoning is usually included in AI (Lean4 has tactics so it qualifies as such) but it's also quite different from the ML stuff that's the more usual kind of AI these days.

rprenger 3y ago
You can have both! LeanDojo: Theorem Proving with Retrieval-Augmented Language Models https://arxiv.org/abs/2306.15626 https://arxiv.org/abs/2306.15626 (shameless plug)
alexvitkov 3y ago
Things usually stop being considered as AI when they start working.

julianeon 3y ago

Now that you mention it, Tao did say he used ChatGPT to help teach himself Lean. https://x.com/8teapi/status/1713867160886599920?s=46&t=4jd61tn6MlpOFUFSrupxWg https://x.com/8teapi/status/1713867160886599920?s=46&t=4jd61...

svat 3y ago
Instead of a twitter post of screenshots of it, the direct link to Tao's Mathstodon is: https://mathstodon.xyz/@tao https://mathstodon.xyz/@tao He's been posting about it since Oct 9: https://mathstodon.xyz/@tao/111206761117553482 https://mathstodon.xyz/@tao/111206761117553482 > I have decided to finally get acquainted with the #Lean4 interactive proof system (using AI assistance as necessary to help me use it), as I now have a sample result (in the theory of inequalities of finitely many real variables) which I recently completed (and which will be on the arXiv shortly), which should hopefully be fairly straightforward to formalize. I plan to journal here my learning process, starting as someone who has not written a single line of Lean code before. There are several posts mentioning how GPT has been useful (though not always) at suggesting things, including one linking to this transcript with ChatGPT: https://chat.openai.com/share/857353ad-a05b-4f9e-bb10-55f15a2bd871 https://chat.openai.com/share/857353ad-a05b-4f9e-bb10-55f15a...