Viewing profile — 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:…

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…

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://g…

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…

> 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 abo…

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 concrete…

> $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/ac…

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…

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 be…

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 …

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 …

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://sigb…

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 J…

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/sands…