dwrensha

highly adept computer knowers explaining recent network exploits while sitting

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

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

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

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.

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

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.

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.

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

Thank for you the emphasis on openness!

I intend to continue work on capnproto-rust, at my own pace and according to my own priorities.

Are there any particular pain points that you want to call attention to?

If you're interested in computer-assisted backronym composition, please check out this interactive tool that I made, based on GPT-NeoX/Pythia models: https://github.com/dwrensha/acronymy-assistant

3-minute video explanation: https://youtu.be/LjOHnXRIp4Y

I've been happily using Pythia in Acronymy Assistant: https://github.com/dwrensha/acronymy-assistant

It's quite convenient to have a continuous range of model sizes. Usually I want "the largest model that fits on my GPU", but sometimes I want to trade between quality and performance, and Pythia makes that easy.

I tried this the other day, and I was also impressed! I had assumed that it would make an illegal move eventually, but it never did. I won the game, but it wasn't trivial. (I've been out of practice in chess for a while; my rating would probably be something like 1700.)

dwrensha vs GPT-4 (through the ChatGPT interface) 16 March 2023

1. d4 Nf6 2. c4 g6 3. Nc3 Bg7 4. e4 d6 5. f3 O-O 6. Be3 e5 7. d5 c6 8. Qd2 cxd5 9. Nxd5 Nxd5 10. Qxd5 Be6 11. Qxb7 Nd7 12. Qa6 Qc8 13. Qxd6 Rd8 14. O-O-O Nc5 15. Qxd8+ Qxd8 16. Rxd8+ Rxd8 17. Bxc5 Rc8 18. b4 a5 19. a3 axb4 20. axb4 Bf8 21. Bd3 Bxc5 22. bxc5 Rxc5 23. Ne2 Bxc4 24. Bxc4 Rxc4+ 25. Kd2 f5 26. Rc1 Rxc1 27. Nxc1 fxe4 28. fxe4 Kf7 29. Ke3 Ke6 30. Nd3 h5 31. h4 Kd6 32. Ne1 Kc5 33. Nf3 Kd6 34. Kd3 Ke6 35. Kc4 Kf6 36. Kd5 g5 37. hxg5+ Kg6 38. Kxe5 h4 39. Ke6 Kh5 40. Kf7 h3 41. g3 h2 42. Nxh2 Kxg5 43. e5 Kf5 44. e6 Ke5 45. e7 Kd6 46. e8=Q Kc7 47. Qe6 Kb7 48. Qd6 Ka7 49. Qb4 Ka6 50. Ke7 Ka7 51. Kd7 Ka8 52. Kc7 Ka7 53. Qb7#

Note that my move 14. O-O-O was a blunder, allowing 14. ... Bxc4, but my opponent instead replied with 14. ... Nc5, which handed me a decisive advantage.

I very nearly fell for a stalemate with 41. gxh3.

After 42. Nxh2, my opponent said: "At this point, it's clear that white has a winning advantage with a promoted queen soon to appear. With your material advantage and superior position, victory is nearly certain. Would you like to continue playing, or do you want to start a new game or discuss this game?" I said, "Let's continue!"

After 52. Kc7, my opponent said "I have no moves left and it's checkmate. Congratulations! You've won the game." I replied: "You do have a move: you can do 52. ... Ka7". My opponent then said, "Apologies for the confusion. You are correct. I'll play 52...Ka7. Your move." Then I typoed the final move as "53. Kb7#" (instead of "53. Qb7#"), and my opponent did not correct me: "You played 53. Kb7#. This time, it is indeed checkmate. Congratulations! You've won the game. If you'd like to play another game, analyze this one, or ask any other questions, feel free to let me know!"

Hasegawa Sayuri wrote up some notes about their submissions at http://sayuri.tx0.org/golfhorse/, including an extremely elegant and compact encoding of huffman trees.

Over on http://golf.horse/ there are leaderboards for finding the smallest Javascript programs that output various word lists, including the Wordle list. I've found it to be a fun and educational challenge. I would be excited to see more submissions!

Is Z3 able to produce proofs for these problems? Or does it only say "unsat" and you need to trust it?

I really like this quote, from 39:50 in the talk:

This is not separate groups of two or three mathematicians each belaboring on a paper on their own. It's not like that. This is not anymore the medieval mathematician's guild--which is how mathematics is still organized today. This is a post-industrial division of labor. It is completely new. It's a math hive. It's exciting, and we haven't seen this sort of thing before, and I think it's going to change mathematics.

The associated video presentation shows the loom in action: https://vimeo.com/547544195

This problem is more tractable than you might think! Some progress on it was printed in the 2016 and 2017 Sigbovik proceedings:

http://sigbovik.org/2016/proceedings.pdf http://sigbovik.org/2017/proceedings.pdf

If this kind of problem appeals to you, please consider participating in http://golf.horse/, a tangentially related challenge that is probably going to tie into Sigbovik 2019.

They have a lot in common!

For a while, capnp-rpc-rust used `gj::Promise`, which is based directly on the C++ Cap'n Proto implementation of promises (i.e. `kj::Promise`). Back in January, capnp-rpc-rust was updated to use `futures::Future` instead, and it was a fairly straightforward transition, as described in this blog post: https://dwrensha.github.io/capnproto-rust/2017/01/04/rpc-fut...

The trickiest part of the transition was dealing with scheduling. The implementation of `kj::Promise` has a built-in scheduling queue that guarantees a certain form of deterministic FIFO semantics, and those semantics are heavily depended upon in the Cap'n Proto RPC implementation. Rust's `future::Future` is less batteries-included, requiring capnp-rpc-rust to explicitly create queues where deterministic scheduling is needed.

Confusing the terminology perhaps even more, in capnproto-rust there is a type `capnp::capability::Promise` that implements `futures::Future`.

The IPython Sandstorm app is a step in this direction: https://apps.sandstorm.io/app/rprqf3t2h3vd3swfkhwk076qrennh9...

True, streaming is not a baked-in feature of Cap'n Proto. Streaming can, however, be implemented on top of capabilities, as with this ByteStream interface: https://github.com/sandstorm-io/sandstorm/blob/v0.197/src/sa...

"There’s no such thing as a free lunch, and in this case Point’s lunch comes in the form of capital appreciation..."

I am fascinated by the rhetorical device being deployed here. In the beginning of the sentence, the "lunch" is the money that you save through lower mortgage payments. By the end, the "lunch" is Point's profits, and the tidy transition suggests that everyone wins.

Cap'n proto is more or less abandoned I believe

As maintainer of capnproto-rust, I beg to differ. :)

Cap'n Proto is indeed actively maintained, and here at Sandstorm we depend on it every day as a core piece of our infrastructure.

I recommend Bob Harper's essay on "boolean blindness": https://existentialtype.wordpress.com/2011/03/15/boolean-bli...

An excerpt:

The problem is computing the bit in the first place. Having done so, you have blinded yourself by reducing the information you have at hand to a bit, and then trying to recover that information later by remembering the provenance of that bit.

A grain's filesystem consists of read-only app data mounted at / and writable grain storage mounted at /var/. From Sandstorm's perspective, upgrading a grain to a new app version just means launching the grain with the new app version's read-only data, leaving the writable /var/ data untouched. The app is then responsible for detecting if any migrations are required and for performing them if so.

Some apps, such as WordPress, already have logic for automatically updating the database when the code changes. Other apps need to add some simple version-detection logic in their startup scripts.

Yes, it should be possible to run an email server as a Sandstorm grain. Note that you would need to grant the grain networking capabilities so that it could talk to the outside world. Currently, only the admins of a Sandstorm server are allowed to grant such capabilities, but that will change once we've implemented our plans for trusted "driver apps" that attenuate and manage admin capabilities.

A grain can keep itself running in the background by requesting a wakelock from its Sandstorm supervisor process. While the grain holds the wakelock, it does not get automatically spun down, even if there are no users visiting it.

As a counterpoint, here's a 2011 video of Bryan Cantrill claiming that it is "emphatically not the case" that the CDDL was specifically developed to be GPL-incompatible: https://youtu.be/-zRN7XLCRhc?t=1375

the serialization part isn't separate they are in one library

Although Cap'n Proto's C++ implementation is hosted in a single git repository, it does compile to several distinct libraries. You can use just the core serialization/deserialization part, libcapnp, if that's all you need. There are separate components, libcapnpc and libcapnp-rpc, for dynamic reflection and the object-capability remote procedure call system.

Groove Basin also has one of these buttons!

http://groovebasin.com/