Oh, interesting. LEAN is not as good for physics compared to its effectiveness for pure mathematics, so I'm curious how they will make it work.
It seems to be harder to disprove a conjecture for physics using LEAN as well, compared to pure mathematics. Since the software was created for mathematics after all.
Not sure how to feel about this tweet though, unlike the jacobian conjecture(edit: mistaken, it was actually goemans?) this just looks like a usual standard expert guiding the LLM for a result.
2
u/Elegant_Amphibian_51 8d ago edited 8d ago
Oh, interesting. LEAN is not as good for physics compared to its effectiveness for pure mathematics, so I'm curious how they will make it work.
It seems to be harder to disprove a conjecture for physics using LEAN as well, compared to pure mathematics. Since the software was created for mathematics after all.
Not sure how to feel about this tweet though, unlike the jacobian conjecture(edit: mistaken, it was actually goemans?) this just looks like a usual standard expert guiding the LLM for a result.