4 ms·

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

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?

ibarrajo 3mo ago
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
- iib 3mo ago
  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?
  - olmo23 3mo ago
    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.
    - auggierose 3mo ago
      Or we just don't use LEAN but something better.
      - rowanG077 3mo ago
        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.
        auggierose 3mo ago
        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).
        deleted 3mo ago
        [deleted]
        baq 3mo ago
        pay attention to this one https://higherorderco.com/ https://higherorderco.com/ and wait for bend2 announcements
pja 3mo ago
Some speculation in this Claude chat: https://claude.ai/share/22abed98-d9af-43c5-9881-b19e009a07b0 https://claude.ai/share/22abed98-d9af-43c5-9881-b19e009a07b0 linked from here: https://x.com/b_shrir/status/2079094004885668003?s=20 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.
- Davidzheng 3mo ago
  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
  - Davidzheng 3mo ago
    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...
    - jlev1 3mo ago
      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.

ibarrajo 3mo ago

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

iib 3mo ago
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?
- olmo23 3mo ago
  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.
  - auggierose 3mo ago
    Or we just don't use LEAN but something better.
    - rowanG077 3mo ago
      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.
      - auggierose 3mo ago
        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).
        deleted 3mo ago
        [deleted]
      - baq 3mo ago
        pay attention to this one https://higherorderco.com/ https://higherorderco.com/ and wait for bend2 announcements

pja 3mo ago

Some speculation in this Claude chat: https://claude.ai/share/22abed98-d9af-43c5-9881-b19e009a07b0 https://claude.ai/share/22abed98-d9af-43c5-9881-b19e009a07b0 linked from here: https://x.com/b_shrir/status/2079094004885668003?s=20 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.

Davidzheng 3mo ago
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
- Davidzheng 3mo ago
  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...
  - jlev1 3mo ago
    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.