ControlsFreak
No bio...
User ID: 1422
Posting separately and prior to the above, so it appears separately and below; this is much less important.
IMHO, this topic is a culture war topic (or at least, it can be, depending upon the presentation). Given that premise, the root comment is a nearly contentless bare link with a one liner snipe of the commenter's outgroup. For example questions, what is "it" and what does it mean for "it" to be "over"? It is plausible that these sorts of questions could have coherent answers that make the original comment benign, but they were not included in the original.
An alternative interpretation is that it is a "First"-post, though I would still probably characterize it at first impression as being paired with a one liner snipe of the commenter's outgroup.
Indeed, I think that the same sense that there even is such a thing as a commenter's "outgroup" on the topic in an indicator in favor of the premise that the topic (or at least a presentation of the topic such as this) is culture war.
EDIT: I should clarify that I am NOT asking for the comment to be modded. I am not entirely confident of my interpretation, and I'm not at all confident that the mods would think so, either. I did not report it because I don't have a strong opinion that it should be modded. I am merely expressing my opinion on some things that I did not like, and I am very open to contrary perspectives.
This is quite exciting! Some scattered thoughts.
I definitely had the sense that we had hope for this type of thing, since math is (mostly) mechanically-verifiable. Lean is about to be getting even more attention than it had before, and it's important that these all come with Lean code attached. That said, my understanding is that it is still possible to do somewhat sketchy things in Lean. I'm expecting a lot more folks will see how important that concern is and really focus on either shoring it up or put together some set of principles like, "If you proof has X component in Lean, we're going to unfortunately simply discount it for now." But most results that come with Lean code will probably be just fine. (I certainly have no reasons to doubt any of these particular results, myself. Nor do have strong personal opinions about the edges of where possibly sketchy things can be done in Lean.)
On the use and human interpretability of results. This question is not new. Take, for example, the massive human-generated proof of Fermat's last theorem or the exhaustive computer-generated proof of the Four Color Theorem. Many many folks don't actually understand these proofs. Perhaps no one "understands" the proof of the Four Color Theorem, whereas at least the proof of Fermat's last theorem is understood well enough by an extremely small group of folks.
Using those results is easy. You don't have to understand them! If you're working on a problem, and you see that it would be useful for one of those things to be true, congrats! You can just use a pointer to the fact that it's true and move on. This is an unalloyed good.
Understanding those results is another matter. I was looking at a paper recently with some collaborators, and it was one of those situations where we were just failing to have much intuition about how to think about certain parts. (FYI, I think this paper was human-generated, but I don't know.) Multiple people in the group suggested that a few things could be, "They just tried a bunch of options, and found one where they could make the computation work out." And that's fine. I've done that before. Plenty of methods include, "You can just try stuff, and if one works, great!" I also happened to afterward figure out a different way to describe the same thing in a way that made intuitive sense out of it, which was extra neat. Maybe if we bang our head against their paper for long enough, we'll be able to find a way to make intuitive sense out of it, too. Maybe an LLM will help! Tao recently mentioned that he had a discussion with an LLM to help him grab some additional intuition around the counterexample to the jacobian conjecture.
At least in the near term, there will probably be a fair number of LLM-produced proofs that people look at and say, "How the hell does that work?" Plenty of time will be spent trying to understand them. Are there new concepts in there? Can you relate it to other math? Can you simplify it and make it more intuitive? Does something in the method raise new interesting questions?
Which leads me to the most hazy part; the somewhat longer term. Will LLMs be able to consistently make intuitive sense of their proofs for humans? Will they be able to help us understand the connections or identify new questions that we would understand as being interesting that are now relevant?
I certainly don't know how to prognosticate all that well, but I do think of some analogies to another domain that is (mostly) verifiable and where computers already significantly outperform humans - chess. Humans still try to understand something from the superhuman output of chess engines. Unfortunately, I can't find it immediately, but I very recently read (as in the last couple weeks, I believe) an argument that top human grandmaster play has barely improved outside of the opening phase, where folks are memorizing more and more of the output of engines. I'm not sure I believe this analysis (I didn't dig into the details of the methodology, and I can imagine plenty of methodological difficulties), but that's something somewhere in my mind. Another thing is that chess has one single extremely well-defined goal: win the game when you can, otherwise draw. This collapses neatly at any particular point in time to, "What is the objectively best move for this game state?" It is relatively easy to accept that the computer is just flatly going to estimate that far better than we are. It's harder to understand the reasons why that is the best move. It's harder (not necessarily impossible, but harder) to take a variety of examples like this from a computer and have a sense for how to built it into a broader understanding of the game. It's harder to make connections like, "The computer seems to value space in positions like X and Y, but not Z; why is that?"
We have plenty of mathematical "positions" teed up for this type of tool. We can hopefully just ask the LLM what the objective evaluation of these "positions" are. Where else it goes, how we understand the whole thing, and what we can do with it are open and exciting questions.
More options
Context Copy link