dwrensha

Joined 13 years ago

Karma

319

Submissions

Member since

Jul 20

David Renshaw

https://dwrensha.ws

View on Hacker News

Recent submissions

Comment · 2 months ago

ranksunbounded has added a comment on the curve: "it was Claude, with Levent Alpöge and Ava Howell!"

Comment · 2 months ago

I'm the maintainer of the linked website.

This morning, a mysterious user named "ranksunbounded" submitted the linked curve, which has rank at least thirty. This breaks the previous record of 29 found by Elkies and Klagsbrun in 2024.

Nobody knows whether it is possible to achieve arbitrarily high ranks.

Comment · 1 year ago

highly adept computer knowers explaining recent network exploits while sitting

Comment · 1 year ago

Where do you see any mention of GPT?

The computer-assisted component of the Noperthedron proof is a reasonably small sagemath program that was (as far as I know) written by humans: https://github.com/Jakob256/Rupert

Perhaps you have confused this article with a recent unrelated announcement about a vibe-coded proof of an Erdos conjecture? https://borisalexeev.com/pdf/erdos707.pdf

Comment · 1 year ago

Moritz Firsching made an STL file: https://github.com/mo271/models/commit/85495b9329be3455a5e3c...

Comment · 1 year ago

> David Renshaw recently gave a formal proof in Lean that the triakis tetrahedron does have Rupert's property

That's me!

This result appears to be significantly harder to formalize.

Steininger and Yurkevich's proof certificate is a 2.5GB tree that partitions the state space into 18 million cells and takes 30 hours to validate in SageMath.

Formalizing the various helper lemmas in the paper does seem achievable to me, but I suspect that applying them to all of the millions of cells as part of a single Lean theorem could present some significant engineering difficulties. I think it'd be a fun challenge!

If that turns out to be infeasible, an alternate approach might be: we could write a Lean proof that the 2.5GB tree faithfully encodes the original problem, while still delegating the validation of that tree to an external SageMath process. Such a formalization would at least increase our confidence that there are no math errors in the setup. A similar approach was taken recently by Bernardo Subercaseaux et al in their recent paper where they formally verified a SAT-solver encoding for the "empty hexagon number": https://arxiv.org/abs/2403.17370

Comment · 1 year ago

Last month, before this result came out, the question "Is Every Convex Polyhedron Rupert?" was added as a formal Lean statement to Google's Formal Conjectures repository:

https://github.com/google-deepmind/formal-conjectures/blob/1...

I wonder how feasible it would be to formalize this new proof in Lean.

Comment · 2 years ago

About half of the problems in Compfiles have complete solutions. They are marked by the checkmarks in the list at https://dwrensha.github.io/compfiles/index.html .

As far as I know, based on published systems like LeanDojo [1] and Magnushammer [2], computers today can only solve a small handful of the very easiest of these problems (like maybe Imo1959P1).

[1] https://leandojo.org/

[2] https://arxiv.org/abs/2303.04488

Comment · 2 years ago

> These puzzle problems are quite simple (for computers) if you have a formalization.

That may be true someday, but it's not yet! That's exactly what the IMO Grand Challenge is about, and nobody has gotten close to solving it.

Comment · 2 years ago

The IMO Grand Challenge is "formal to formal" -- a solver is given the problem specified in the Lean programming language, and must produce a solution in Lean. To see more concretely what this setup might look like, check out https://github.com/dwrensha/compfiles.

The AI MO prize is "informal to informal" -- a solver is given a problem in natural language and must produce a solution in natural language.

My belief is that the best way to get to "informal to informal" is to first solve "formal to formal", but not everyone thinks so.

Comment · 2 years ago

> $5mn will be awarded to the first publicly-shared AI model

Thank for you the emphasis on openness!