Gemini with Deep Think achieves gold-medal standard at the IMO • Hacker News Board

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#251

Post by daxfohl » Tue, Jul 22, 2025, 5:40 PM UTC

mietek wrote: post #174

nicf wrote: post #148

Earlier quoted context omitted.

I'm a mathematician, although not doing research anymore. I can maybe offer a little bit of perspective on why we tend to be a little cooler on the formal techniques, which I think I've said on HN before. I'm actually prepared to agree wholeheartedly with what you say here: I don't think there'd be any realistic way to produce thousand-page proofs without formalization, and certainly I wouldn't trust such a proof wit…

A proof written in a formal language can absolutely be illuminating to a human, but you have to pick the correct formal language and ecosystem. Writing proofs in Agda is like writing programs in a more expressive variant of Haskell. Abelson said that “programs must be written for people to read, and only incidentally for machines to execute”, and by the Curry-Howard isomorphism, proofs can be seen as programs. All th…

I see axiom of choice, and really LEM, as logic's equivalent to limit points in calculus. No, you can't calculate 0/0, but here's what the answer would be if you could. No, you can't prove the truthiness of this statement, but here's what it would be if you could.

I guess one could work in a brand of math whose axioms make defining and using limits impossible, which, maybe if formalization came before the invention of calculus, would make some 17th-century mathematicians feel more comfortable. Though I imagine it would make progress in physics challenging. I think the same about LEM/AoC. Given that almost every element in the power-set of reals is non-measurable, maybe stuff like Banach-Tarski is actually fundamental in real physics: it can't be predicted or computed, but it can be observed.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#252

Post by daxfohl » Tue, Jul 22, 2025, 6:00 PM UTC

lblume wrote: post #170

nicf wrote: post #148

Earlier quoted context omitted.

I'm a mathematician, although not doing research anymore. I can maybe offer a little bit of perspective on why we tend to be a little cooler on the formal techniques, which I think I've said on HN before. I'm actually prepared to agree wholeheartedly with what you say here: I don't think there'd be any realistic way to produce thousand-page proofs without formalization, and certainly I wouldn't trust such a proof wit…

I have always wondered about what could be recovered if the antecedent (i.e. in this case the Riemann hypothesis) does actually turn out to be false. Are the theorems completely useless? Can we still infer some knowledge or use some techniques? Same applies to SETH and fine-grained complexity theory.

It depends. The most likely scenario would be that RH holds except in very specific conditions. Then, any dependent theorems would inherit the same conditions. In many cases, those conditions may not affect the dependent theorem, so they'd still be completely valid. In some cases, those conditions may make the dependent theorem useless, like if RH was "all numbers are even", and your theorem was "all numbers % 2 equal zero, because we know even numbers % 2 are zero and we assume RH", then the exception to RH "except odd numbers" would make your theorem devolve to "all numbers % 2 are zero except the odd ones, because we know even numbers % 2 are zero", which is obviously just a restatement of an existing statement.

In other cases, the new condition affects your theorem but doesn't completely invalidate it. So you can either accept that your theorem is weaker, or find other ways to strengthen it given the new condition.

That's all kind of abstract though. I'm not an expert on RH or what other important math depends on it holding up. That would be interesting to know.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#253

Post by riku_iki » Tue, Jul 22, 2025, 8:23 PM UTC

mietek wrote: post #174

nicf wrote: post #148

Earlier quoted context omitted.

I'm a mathematician, although not doing research anymore. I can maybe offer a little bit of perspective on why we tend to be a little cooler on the formal techniques, which I think I've said on HN before. I'm actually prepared to agree wholeheartedly with what you say here: I don't think there'd be any realistic way to produce thousand-page proofs without formalization, and certainly I wouldn't trust such a proof wit…

A proof written in a formal language can absolutely be illuminating to a human, but you have to pick the correct formal language and ecosystem. Writing proofs in Agda is like writing programs in a more expressive variant of Haskell. Abelson said that “programs must be written for people to read, and only incidentally for machines to execute”, and by the Curry-Howard isomorphism, proofs can be seen as programs. All th…

I would argue is that some portion of ecosystem should be readable by humans.

In programming engineering we already have this: there is human readable high-level code, and there is assembler and lots of auto-generated code.

In proof system we could have the same: key concepts/theorems should be encoded in human readable form, but no need for human to read through millions of generated lines.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#254

Post by lacker » Wed, Jul 23, 2025, 10:00 PM UTC

valicord wrote: post #233

lacker wrote: post #179

Earlier quoted context omitted.

Typically formalization is actually harder than solving a problem. You almost always solve before formalizing. And it can be surprisingly hard to formalize problems that are easy to solve. For example, is there a polygon of area 100 that you can fit 99 circles of area 1 inside it, without overlapping? Yes, obviously, it's very easy to prove this informally. Now try formalizing it! You will find it takes a while to fo…

The polygon claim is not at all obvious to me, how do you prove it?

Draw 99 circles in a row, then draw a separate polygon around each one with only a teeny amount of excess area, then connect those polygons with teeny little connectors to make it a single polygon. When I say "teeny", you can make those arbitrarily small, so you can certainly fit them under 1 total area.

Okay, it's maybe not "obvious" in a regular human sense, but in a graduate math class you could claim this was "obvious". It would be pretty clear if I were drawing a diagram on a whiteboard. I would definitely take less time proving this to a human, than formalizing it.