[opan]

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

[julianeon]

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=4jd61...

[svat]

Instead of a twitter post of screenshots of it, the direct link to Tao's Mathstodon is: https://mathstodon.xyz/@tao

He's been posting about it since Oct 9: 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-55f15a...

[sebzim4500]

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

[zozbot234]

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.

[alexvitkov]

Things usually stop being considered as AI when they start working.

[rprenger]

You can have both! LeanDojo: Theorem Proving with Retrieval-Augmented Language Models https://arxiv.org/abs/2306.15626 (shameless plug)