My point is that pushing for human understanding as the primary goal assumes an answer to an empirical question that we don't yet have evidence for. How do we know that human understanding is the right instrumental goal, as opposed to solving open problems as fast as possible? Even if we think human understanding has intrinsic value, how do we know which approach will maximize human understanding in the long run?
The idea that all meaningful questions can be answered empirically is known as "verificationism" and is philosophically quite dubious.
This is an empirical question, right? We could have three teams of researchers, team A focusing purely on understanding, team B focusing purely on solving problems, and team C focusing on a combination of the two. See which one makes the most breakthroughs on problems we actually care about.
I respect Tao and I believe he's trying to think deeply about the issues, but a lot of his thinking seems to revolve around preserving the current roles and prestige of mathematicians, and also makes a lot of assumptions about the capabilities of AI years or decades into the future.
Another example: early in his career, Scriabin sounded a lot like Chopin. Later in his career, though, his music turned into something truly original and one-of-a-kind. It seems necessary to start out imitating your idols, but at some point true artists aren't content with imitating and have to find their own voice.
Where is the evidence of saturation of need? Most of the big problems remain unsolved in medicine, biology, chemistry, physics, and engineering. Even if we eliminated war, poverty, authoritarianism, and economic instability, we would still have more problems to solve.
I was surprised when I heard Tristan Buckmaster, an expert on fluid dynamics, say that we still don't understand basic things from first principles like how airplanes generate lift.
You're right, I probably could have been clearer and more nuanced in my wording. In the context of the comment I was responding to, I was pushing back against a claim of "free speech absolutism" which I don't really see as free speech absolutism at all. I see GGP's attitude more as a form of anti-criticism or what I would call "neutrality fundamentalism". I was probably a bit reactive because I consider myself a free speech absolutist, but in the sense of being against all government censorship, not necessarily private entities exercising their right to criticize or associate with whoever they want.
I agree that some forms of cancellation are illiberal and anti-free speech. But a lot of the time, what gets called "canceling" or "shutting down" are themselves forms of free speech and freedom of association. Freedom of speech doesn't mean that everyone is entitled to being taken seriously, or having their opinions broadcast in private venues and publications, or being immune from criticism, mockery, protest, or social ostracization. A lot of people who call themselves free speech absolutists think that none of this should be allowed and that all ideas deserve an equal hearing.
Free speech is about government making certain forms of speech illegal. Criticism of people/ideas and freedom of association are themselves acts of free speech.
I don't put much weight on guilt by association. She's led public protests against the Maduro regime and had to go into hiding to escape imprisonment. She's advocated for free and fair elections, rule of law, separation of powers, civil liberties, decentralization, private property, and competitive markets. Can you explain how those actions and ideas are authoritarian?
It goes against the principles of classical liberalism: rule of law, civil liberties, and limited government. I don't think we should just shrug our shoulders and say that it's fine if some countries want to strip rights from people on the basis of race or economic class.
It's a false equivalence. If I design a censorship-resistant network, it doesn't imply that I endorse everything flowing through that network. And just because I'm in favor of free speech doesn't mean I can't criticize the speech of others as a private citizen or organization.
Free speech absolutists can still have opinions, criticize others, and choose who to associate with. They're not advocating for censorship or legal penalties for speech.
I think people are making a mistake when they view the Peace Prize as an evaluation of a person's character or their entire career. Often it's targeting specific negotiations or treaties, which in retrospect were failed attempts at peace. This applies to Kissinger in the case of the Paris Peace Accords, Begin/Sadat for the Camp David Accords, Arafat/Peres/Rabin for the Oslo Accords, etc.
Those are statements about auto-formalization and the NL proof. They're saying that further work needs to be done on verifying whether the Lean and NL proofs are equivalent, which is completely valid. But they're not disputing that the Lean formalization is a correct statement of the Millennium Prize problem. You can see in the link I provided (and the original pull request) that it was written by humans, reviewed by human experts, and is completely independent of the OpenAI effort.
Sounds like an opportunity for a good engineer to come in and write something with the same functionality that runs locally and efficiently. The claim that it's wasteful only holds water if the non-wasteful solution exists and can accomplish the same tasks.
>or if the initial statement in Lean is correct. I suppose that's obvious.
Is it obvious? The formal statement that Astra proved was written by a human, submitted to a DeepMind repository, and reviewed by human experts in a pull request. It's completely independent of OpenAI's effort. No expert in PDEs or formal verification has disputed it as far as I'm aware.
María Corina Machado has stood up against authoritarianism in Venezuela for more than a decade. I don't think awarding the prize should require that the recipient is a perfect person or holds all of the "correct" opinions according to bystanders who have no skin in the game.
I don't care if Anthropic keeps using it, it's part of their brand at this point. The thousands of other developers using Claude Code to generate designs should not just accept the default output, which looks very Anthropic-ish, and actually put some effort into polishing and differentiating their product. It has nothing to do with usability and everything to do with a basic sense of good taste and aesthetics.
According to economic theory, price controls produce shortages. It's likely that capping transaction fees would have unintended consequences, for instance excluding customers from being able to get a credit card in the first place. I'm not against all regulation, but I think we should prefer market-based solutions that remove barriers to entry and that allow more companies to compete in the space.
Anthropic's aesthetic looks good by pre-AI design standards, but it's so overused now that I find it off-putting. It's like the 2026 equivalent of the Twitter bootstrap CSS from 15 years ago.
This, and in addition to dogfooding, incentivizing employees to be more effective with the cheaper models. A lot of problems don't need anything fancy, but it takes more brain power and engineering effort to make that work. By default humans will take the path of least resistance if it's available.
Wiles' proof was informal and couldn't be checked by a computer. In this case, the experts need to check 300 lines of Lean code (mostly comments) and confirm that it formalizes the problem statement correctly. There are papers building on the solution and analyzing it for more general versions of the problem, which suggests that the PDE community has already accepted it and moved on.
All of the reasons you listed for peer review are valid. The broader point is that peer review can happen outside of academic journals, and nobody has an incentive to submit to them who isn't trying to play the academic prestige game. For a significant example, see the history of Perelman's proof of the Poincaré conjecture.
I didn't say peer review is low quality; just that it's not necessary or sufficient to determine the truth. Ultimately the OpenAI proof stands or falls on things that have been audited externally, namely the formalization of the problem in Lean and the correctness of the Lean software. There's no incentive for OpenAI to submit to a peer-reviewed journal when they don't need to play the academic prestige game. TFA is an example of peer review in action: they're analyzing the proof and finding points to criticize.
The claim is about the equivalence between two proofs and says nothing about the correctness of either proof. This seems to be confusing a lot of people.
Does that contradict what I said? In that quote, it says that the NL proof does not correspond to the Lean proof. However, the statement of the theorem in Lean is independent from the NL proof. It comes from a DeepMind repository, which as far as I'm aware has been accepted by the community as a valid formalization of the original Clay Institute statement.