dwrensha

5 ms·

1.
by dwrensha 29d ago
ranksunbounded has added a comment on the curve: "it was Claude, with Levent Alpöge and Ava Howell!"
2.
by dwrensha 1mo 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
3.
by dwrensha 11mo ago
highly adept computer knowers explaining recent network exploits while sitting
4.
by dwrensha 11mo 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 Pe
5.
by dwrensha 11mo ago
Moritz Firsching made an STL file: https://github.com/mo271/models/commit/85495b9329be3455a5e3c...
6.
by dwrensha 1y 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 certifi
7.
by dwrensha 1y 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&#
8.
by dwrensha 3y 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 Lean
9.
by dwrensha 3y 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.
10.
by dwrensha 3y 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 htt
11.
by dwrensha 3y ago
> $5mn will be awarded to the first publicly-shared AI model Thank for you the emphasis on openness!
12.
by dwrensha 3y ago
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?
13.
Run-time reflection in capnproto-rust(dwrensha.github.io)
3 points by dwrensha 3y ago|0 comments
14.
by dwrensha 3y ago
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 vi
15.
by dwrensha 3y ago
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 th
16.
by dwrensha 4y ago
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
17.
by dwrensha 5y ago
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.
18.
by dwrensha 5y ago
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
19.
by dwrensha 5y ago
Is Z3 able to produce proofs for these problems? Or does it only say "unsat" and you need to trust it?
20.
by dwrensha 5y ago
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-
21.
by dwrensha 5y ago
The associated video presentation shows the loom in action: https://vimeo.com/547544195
22.
by dwrensha 8y ago
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/pro
23.
by dwrensha 9y ago
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::Fut
24.
by dwrensha 9y ago
The IPython Sandstorm app is a step in this direction: https://apps.sandstorm.io/app/rprqf3t2h3vd3swfkhwk076qrennh9...
25.
by dwrensha 10y ago
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/v
26.
by dwrensha 10y ago
"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&q
27.
by dwrensha 10y ago
> 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 infrastruc
28.
by dwrensha 10y ago
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. Hav
29.
by dwrensha 10y ago
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
30.
by dwrensha 10y ago
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 all

More ›