iiinova — where your digital self keeps evolving

← back

Open on Bluesky →

Replies

Open on Bluesky →

Replies

dan @danabra.mov · 02/09/2026

okay, it's out github.com/gaearon/conw...

github.com

GitHub - gaearon/conway-refinement: A proof of Conway's refinement conjecture in Lean

A proof of Conway's refinement conjecture in Lean. Contribute to gaearon/conway-refinement development by creating an account on GitHub.

dan@danabra.mov

preparing to publish my vibecoded math lean proof to github and i kinda feel nervous cause what if it's all wrong

151266

Chevindu @chevindu.com · 02/09/2026

I'm sorry I am a child and I'll see myself out.

Says "Surreal numbers and anal..." which is an unfortunate placement of the ellipsis

000

gigaben (ascending) @thebenku.bsky.social · 02/09/2026

this is great, congrats! have you been able to find any interesting/enlightening takeaways from the proof? i keep thinking back to the transcript of terry tao talking with an llm about some lean (i think?) proofs and it really seemed like a profitable endeavor to explore these artifacts w/ llm

100

Maxine 💃🏼 @maxine.science · 02/09/2026

A first pass on this: The types are right so I buy it proves the thing; I buy it more because the machinery is very heavily from a couple groups and the proof is mostly, from what I can see, carrying those tools through to edges and ugly parts they (for good economic reasons) hadn’t attended to. 1/

Maxine 💃🏼@maxine.science

if you want a pre-pub peer review i'm game, i'm a mathematician who does vibe-Lean :)

140

oliver @eikopf.com · 02/09/2026

the proof map seems to imply that section 13 isn't relevant to the final result?

010

sasha @gudulin.com · 02/09/2026

congrats dan! this is cool :) got inspired and started workin on a formal verification in lean for plotting time-series (based on this paper arxiv.org/pdf/2108.039...)

arxiv.org

020

Samuel @samuel.fm · 02/09/2026

that's awesome, fingers crossed it stands up to review!

090

Sean Newell @sean.thenewells.us · 02/09/2026

omnific integers are giving "go beyond, plus ultra!" from MHA

010

wariziles @riziles.bsky.social · 02/09/2026

Congrats!

000

bjkeefe @bjkeefe.bsky.social · 02/09/2026

Really impressive work.

000

business goose🪿 @goose.art · 02/09/2026

this is way beyond me but it was fun to learn about surreal numbers in the readme :•)

130

dan @danabra.mov · 02/09/2026

how it started

claude: Cards on the table: I pick Conway's arithmetic. Specifically, the question the L'Innocente–Mantova machinery just sharpened to a point — is every irreducible in K((ℝ^≤0)) with infinite support prime? — which, by their reduction, is now exactly equivalent to Conway's 1976 conjecture that any two factorizations of an omnific integer admit a common refinement. It's the last of Conway's own conjectures about his own numbers still standing, and 2026 is ONAG's fiftieth birthday. That's the problem I'd work on.

1140

conputer dipshit @davidcrespo.bsky.social · 02/09/2026

wow. how fun if the mathematicians can confirm it. very nice readme

130

jake @yetanotheruseless.com · 02/09/2026

@littmath.bsky.social, @johncarlosbaez.bsky.social, have you all seen this?

100

jake @yetanotheruseless.com · 02/09/2026

i would imagine you want input from mathematicians, right? do you mind if this gets shared to other platforms where you don't spend time (mast, lnkd, xitter, etc), linking back to here?

130

Matt Hodges @matthodges.bsky.social · 02/09/2026

Excited to go learn about surreal numbers

010