Hacker News Reader

Comment by Davidzheng | Hacker News Reader

I have a question I'm surprised people are not asking: How did Fable find this? Was it like guessing a bunch of families and then solving for possible solutions in those families? Was it clever search? something else?

View on HN

Some speculation in this Claude chat: https://claude.ai/share/22abed98-d9af-43c5-9881-b19e009a07b0

linked from here: https://x.com/b_shrir/status/2079094004885668003?s=20

Very short version: there’s an existing false counterexample in the literature which holds almost everywhere except at a pole. It looks like Fable used this polynomial as a base & extended it in a way that eliminated the pole whilst preserving the structure.

I'm going to paraphrase what GPT told me: Consider the canonical degree 3 (subvariety of the trivial P1 bundle consisting of zeros) cover of the projectivization of homogenous polynomials of degree 3 in 2 variables (so it's a 3fold cover of P^3). The top space is P1 x P2 and if you take a standard affine open of the base and look at the cover over that restricted to a subset where the zero of the cubic is simple you get the map for some choice of coordinates...

I honestly have no idea if it's correct lol I didn't check it (I should given I actually work in AG) but it doesn't look impossible at first sight

here's another version directly from the horse's mouth : "Consider the natural map π: P¹ × Sym²(P¹) → Sym³(P¹), (p, {q,r}) ↦ {p,q,r}. Let R be its ramification divisor and let H ⊂ Sym³(P¹) ≅ P³ be a hyperplane tangent but not osculating to the small diagonal; identify X := (P¹ × Sym²(P¹)) \ (R ∪ π⁻¹(H)) ≅ A³ and Y := Sym³(P¹) \ H ≅ A³. Take π|X: X → Y." This is in fact so simple if correct that someone should have found it after all...

My Claude found a similar description (it phrased it in terms of the natural map from "cubics with a choice of root" to "cubics"). The part that seems not at all simple or obvious is the fact that X is isomorphic to A^3. In your presentation (and more or less similarly in the one my Claude found), X is given as P1 x P2 minus a reducible hypersurface, also I think R itself is reducible since it contains points of the form (p, {p, q}) and (p, {q, q}). Then it takes some calculation to identify X with A^3.

yeah I think it's probably correct -- this is actually insanely simple (except for the fact that the codomain as described is not obvious isomorphic to A^3.

I agree.

on the other hand it's incredible to me as someone who doesn't do computations that GPT took one look and saw the geometry--though it's not saying much we should ask ppl who do AG computations

It’s not that surprising (to me) that it would recognize these features, in that the features it picks up on are intrinsic to the map. Once you have the map, which is generically of degree 3, there’s the locus where the map drops from degree 3 to 2, which contains a big hint because it pops out the equation for the discriminant locus of a cubic. Then there’s the other bit about H, which becomes more apparent from the formula after simplifying things a bit in terms of discriminant. I still don’t yet understand the rest of the calculation, but it’s visibly simpler after you notice the role of the discriminant.

I’m doing this by working all logical steps into lean (formal verification) the quick feedback loop between the AI prose and the Lean verification errors and warnings ensures that its logically consistent.

The issue that remains are two things, ensuring the idea of the proof is actually the thing you want to prove and the interpretation of the results you get. But besides that, everything inside of the kernel checked code is logically consistent

In my experience, lean will show that it's correct, but does it not lose the mathematical intuition that led to the result? As far as my experience goes, that's really hard to encode in lean itself.

Could we maybe get more information about the problem from the LLM trace itself here?

As proofs become more and more complex, we will need two AI pipelines: one to generate the LEAN proof, and a second one to extract useful lessons for mathematicians from the LEAN proof.

Or we just don't use LEAN but something better.

Does anything truly better exist? I'm not a mathematician but I did use Rocq and Lean during university. And I found lean to be better.

No, something truly better does not exist yet, but that doesn't mean that it won't. Lean is young compared to Isabelle or Rocq, but actually quite old in absolut terms (and especially in AI terms).

pay attention to this one https://higherorderco.com/ and wait for bend2 announcements

Reply on news.ycombinator.com