4 ms·

I was worried that Lean4 is a yet another LLM, but it's actually some hard and reliable stuff.

by Dudester230602 3y ago

woolion 3y ago
"Terry Tao finds ChatGPT very helpful to prove new theorems" would actually be bigger news than this one, IMO.
- throwalean 3y ago
  "Terry Tao finds ChatGPT very helpful to formally verify his new theorems" seems to be a true statement. See some of his other recent mathstodon toots.
  - woolion 3y ago
    The point is that LLMs and similar tools tend to be very good at automating the trifle but not very useful at what would be considered really "interesting" work. So while your point is somewhat true [0], as he mentions that these tools could become good enough to do the formal verification part, it's precisely not the interesting part. See [1] and [2]; in particular some things that are very easy to do in real maths can be very challenging in an automated theorem prover, quoting from [2]: >In the analyst's dialect of Mathematical English, this is a one-line proof, namely "by the standard limiting argument". Unpacking this into a formal proof required me to go through a fair bit of the Mathlib documentation [...] It's impressive to be able to do such mathematics in Lean/Coq..; at all, but it is very tedious mechanical work [3]. >It was more tedious than I expected, with each line of proof taking about an hour to formalize So I think that rather proves the point of what LLMs are currently good for, and what tools can help for really difficult tasks, rather than invalidate it. [0] https://mathstodon.xyz/@tao/111305365372766606 https://mathstodon.xyz/@tao/111305365372766606 [1] https://mathstodon.xyz/@tao/111305336701455719 https://mathstodon.xyz/@tao/111305336701455719 [2] https://mathstodon.xyz/@tao/111259986983504485 https://mathstodon.xyz/@tao/111259986983504485 [3] https://mathstodon.xyz/@tao/111305336701455719 https://mathstodon.xyz/@tao/111305336701455719
jamesrom 3y ago
Anything that helps Terence Tao find bugs in his papers is hard and reliable in my books.
OscarCunningham 3y ago
He is finding Copilot useful to help with the formalisation: https://mathstodon.xyz/@tao/111271244206606941 https://mathstodon.xyz/@tao/111271244206606941.
ykonstant 3y ago
The Lean 4 community is quite optimistic about combining LLMs and theorem provers for proof assistance and formalization.

I was worried that Lean4 is a yet another LLM, but it's actually some hard and reliable stuff.

woolion 3y ago

"Terry Tao finds ChatGPT very helpful to prove new theorems" would actually be bigger news than this one, IMO.

throwalean 3y ago
"Terry Tao finds ChatGPT very helpful to formally verify his new theorems" seems to be a true statement. See some of his other recent mathstodon toots.
- woolion 3y ago
  The point is that LLMs and similar tools tend to be very good at automating the trifle but not very useful at what would be considered really "interesting" work. So while your point is somewhat true [0], as he mentions that these tools could become good enough to do the formal verification part, it's precisely not the interesting part. See [1] and [2]; in particular some things that are very easy to do in real maths can be very challenging in an automated theorem prover, quoting from [2]: >In the analyst's dialect of Mathematical English, this is a one-line proof, namely "by the standard limiting argument". Unpacking this into a formal proof required me to go through a fair bit of the Mathlib documentation [...] It's impressive to be able to do such mathematics in Lean/Coq..; at all, but it is very tedious mechanical work [3]. >It was more tedious than I expected, with each line of proof taking about an hour to formalize So I think that rather proves the point of what LLMs are currently good for, and what tools can help for really difficult tasks, rather than invalidate it. [0] https://mathstodon.xyz/@tao/111305365372766606 https://mathstodon.xyz/@tao/111305365372766606 [1] https://mathstodon.xyz/@tao/111305336701455719 https://mathstodon.xyz/@tao/111305336701455719 [2] https://mathstodon.xyz/@tao/111259986983504485 https://mathstodon.xyz/@tao/111259986983504485 [3] https://mathstodon.xyz/@tao/111305336701455719 https://mathstodon.xyz/@tao/111305336701455719

jamesrom 3y ago

Anything that helps Terence Tao find bugs in his papers is hard and reliable in my books.

OscarCunningham 3y ago

He is finding Copilot useful to help with the formalisation: https://mathstodon.xyz/@tao/111271244206606941 https://mathstodon.xyz/@tao/111271244206606941.

ykonstant 3y ago

The Lean 4 community is quite optimistic about combining LLMs and theorem provers for proof assistance and formalization.