cdetrio

I'd be very curious whether such junk lean code could be used to solve Kevin Buzzard's Jacobian challenge: https://gist.github.com/kbuzzard/778bc714030b3e974ab5f403878...

The idea behind the challenge to provide a few lines of human-written/checked scaffolding that defines an "API surface". The API surface is resistant to junk/slop filling out the sorry's. This is supposed to reduce the number of lines that humans have to read to only a handful, while the full valid AI-generated proof is tens of thousands of lines. The challenge was just solved a couple weeks, here's the discussion about it: https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...

Many parallels between this article and another posted today ("Unsubscribe from the Church of Graphs" https://news.ycombinator.com/item?id=47604253). Both are responses to astralcodexten posts, and the vibes felt around anecdata vs statistics.

We found 500 zero-days in ten year old widely used open-source projects. Was that not a demonstration of the catastrophic failure of human debugging capability?

The Duke harness was specifically designed for these puzzles, that's why they don't want to measure it.

My reading of that part in the technical report (models "could be using their own tools behind the model’s API, which is a blackbox"), is that there's no way to prevent it.

But from fchollet's comment here, using tools and harnesses is encouraged, as long as they are generic and not arc-agi specific. In that case, the models should be benchmarked by prompting through claude code and codex, rather than the through API (as from the api we only expect raw LLM output, and no tool use).

Are you prompting the models through their APIs, which are not designed to use tools or harnesses? Or do the "system prompt" results come from prompting into the applications (i.e. claude code, or codex, or even the web front-ends)?

Astrophysicist David Kipping had a podcast episode a month ago reporting that LLMs are working shockingly well for him, as well as for the faculty at the IAS.[1]

It's curious how different people come to very different conclusions about the usefulness of LLMs.

https://youtu.be/PctlBxRh0p4

very interesting, thanks for sharing.

Textbook models typically simulate normal development of an embryo, e.g. A-P and D-V (anterior-posterior and dorsal-ventral) patterning. The question Levin raises is how a perturbed embryo manages to develop normally, both "picasso tadpoles" where a scrambled face will re-organize into a normal face, and tadpoles with eyes transplanted to their tails, where an optic nerve forms across from the tail to the brain and a functional eye develops.

I haven't thoroughly read all of Levin's papers, so I'm not sure to what extent they specifically address the issue of whether textbook models of morphogen gradients can or cannot account for these experiments. I'd guess that it is difficult to say conclusively. You might have to use one of the software packages for simulating multi-cellular development, regulatory logic, and morphogen gradients/diffusion, if you wanted to argue either "the textbook model can generate this behavior" or that the textbook model cannot.

The simulations/models that I'm familiar with are quite basic, relative to actual biology, e.g. models of drosophila eve stripes are based on a few dozen genes or less. But iiuc, our understanding of larval development and patterning of C Elegans is far behind that of drosophila (the fly embryo starts as a syncytium, unlike worms and vertebrates, which makes fly segmentation easier to follow). I haven't read about Xenopus (the frogs that Levin studies), but I'd guess that we are very far from being able to simulate all the way from embryo to facial development in the normal case, let alone the abnormal picasso and "eye on tail" tadpoles.

"Some people become depressed at the scale of the universe, because it makes them feel insignificant. Other people are relieved to feel insignificant, which is even worse. But, in any case, those are mistakes. Feeling insignificant because the universe is large has exactly the same logic as feeling inadequate for not being a cow. Or a herd of cows. The universe is not there to overwhelm us; it is our home, and our resource. The bigger the better." -- David Deutsch

Maybe you saw this paper about that idea - The Genomic Code: The genome instantiates a generative model of the organism.

"Here, we propose a new analogy, inspired by recent work in machine learning and neuroscience: that the genome encodes a generative model of the organism. In this scheme, by analogy with variational autoencoders, the genome does not encode either organismal form or developmental processes directly, but comprises a compressed space of latent variables."

1. https://arxiv.org/abs/2407.15908 2. discussion with the authors https://www.youtube.com/watch?v=6QaMnUBkmz4

Those papers say the virus is natural and wasn't engineered by humans. The OP link is about the theory that origin event is a natural virus escaping from a lab. A wild-type virus specimen obtained from bats in the wild that was being studied in the lab (not engineered or modified in the lab).

related: https://news.ycombinator.com/item?id=21107706 - Number theorist fears many proofs widely considered to be true are wrong (vice.com)

Many futures exchanges are open 24 hours on weekdays (perhaps with 15 minute gaps), but not weekends. Can you link to one that's open on the weekends?

I haven't seen an FX exchange that trades through weekends, since Oanda stopped offering weekend trading back in 2012.[1] Can you link to one?

1. https://www.leaprate.com/news/oanda-suspends-weekend-trading...

Its about who applies AI and for what purpose. Currently, FANG controls all the data and applies AI to maximize ad clicks (the evil paperclip maximizer). "blockchain" is a movement for people who want "take back" their data (re-decentralize the web). They still want the benefits of machine learning on big personalized data sets (but without the annoying intrusions of profit-maximizing EvilCorp).

I mention in the talk that our fuzz tester, Guido Vranken, moved on to fuzzing WAVM (the wasm jit engine used in EOS) after v8. He earned some bounties (only some of them were related to WAVM) and several articles were written about it. I believe WAVM has some constants that can be set low enough to prevent JIT bombs, but I didn't follow the details so I'm not sure. Check out this commit, in particular the changes to WASMSerialization.cpp: https://github.com/EOSIO/eos/commit/af02ebba5d5797b6dcc2f06b...

This is exciting for the Ewasm team (Ethereum WebAssembly). We're hoping this new single-pass compilation in Liftoff won't be vulnerable to JIT bombs, which are wasm modules that take a lot longer to compile than they do to execute. JIT bombs would be DoS attack vectors on Ethereum clients using JIT wasm engines, and we found some v8 JIT bombs through fuzz testing some months ago.

I gave a talk about it back in June. Slides: https://docs.google.com/presentation/d/1n75Mo09HmyruV5S7q0cH... video: https://youtu.be/2eISBAbT3GM?t=1h22m3s

Any update on those new super-accurate GPS chips? [1]

1. https://news.ycombinator.com/item?id=15308771 Super-Accurate GPS Chips Coming to Smartphones in 2018 (ieee.org)

Why is mining an attack chain expensive? If you mine on the honest chain, you earn the block reward for each block you mine. If you mine an attack chain with 49% and your attack fails, then you sacrifice those rewards. Suppose you mine say 10+ blocks with 51%+, over the next three hours while the rest of the network only finds 8 blocks. Then your 10 blocks become the longest chain and you earn the block reward for all 10 of them.

51% attacks on the block proposal mechanism could prevent the PoS commitments from ever becoming finalized (i.e. violate liveness), though.

Requiring more confirmations decreases the probability that a transaction will be reverted, under the assumption that an attacker has < 49% of the hashpower. If you attempt an attack with 49%, then you have a fair chance of mining, say, 6 blocks before the rest of the network. If you get unlucky then you sacrifice those rewards. But if you mine with 51% then your attack chain is (probabilistically) guaranteed to eventually become the longest chain, so there won't be any loss of revenue.

The "Bill bale pale mayo" video is my second favorite after this one https://www.youtube.com/watch?v=JATjMZJuX1c

The article links to tetherreport.com

We vary N from 1 to 24 hours and examine the p-values. [.....] there are a number of periods where the p-values are significantly below 0.05 and we reject the null hypothesis for those periods.

Is it p-hacking to vary N and find low p-values? If its not p-hacking, but a valid analysis with predictive power, then wouldn't it make a good trading strategy to watch the tether wallet and buy btc whenever new issuance happens?

Its easy to go through a couple containers and find/replace a few sensors. But it would be a lot of work for Bob to go through every single yogurt container and corrupt all the sensors.

any signs yet of support for Web Workers?

It actually does say that the Army spent over their budget:

Skidmore got involved last spring when he heard Catherine Austin Fitts, former assistant secretary of Housing and Urban Development, refer to a report which indicated the Army had $6.5 trillion in unsupported adjustments, or spending, in fiscal 2015. Given the Army’s $122 billion budget, that meant unsupported adjustments were 54 times spending authorized by Congress.

I met a couple guys from their team a couple months ago at the ETHWaterloo hackathon (post from then [1]). They presented a contract analytics tool to graph the number and type of function calls, like an etherscan.io but for custom queries/reports. The queries they showed had function names like SireKitten(), it was all quite funny and I assumed the analytics tool was the main product and that the kitty contracts were a joke example. Never would've guessed that it would take off, but I didn't see all the cute avatars then either.

1. https://news.ycombinator.com/item?id=15479945

Univalent Foundations is apparently controversial. It appeared to come to a head a couple years ago when a lively debate played out in the comments of a blog (including a comment by Voevodsky himself): https://mathematicswithoutapologies.wordpress.com/2015/05/13...

Reading the story[1] about Voevodsky, I was reminded of how Bertrand Russell described Gottlob Frege as "almost superhuman":

As I think about acts of integrity and grace, I realise that there is nothing in my knowledge to compare with Frege’s dedication to truth. His entire life’s work was on the verge of completion, much of his work had been ignored to the benefit of men infinitely less capable, his second volume was about to be published, and upon finding that his fundamental assumption was in error, he responded with intellectual pleasure clearly submerging any feelings of personal disappointment. It was almost superhuman and a telling indication of that of which men are capable if their dedication is to creative work and knowledge instead of cruder efforts to dominate and be known. [2]

And how rare it is to see such "exceptionally honest" academic dialogue as Frege's:

Frege starts his analysis by this exceptionally honest comment : "Hardly anything more unfortunate can befall a scientific writer than to have one of the foundations of his edifice shaken after the work is finished. This was the position I was placed in by a letter of Mr Bertrand Russell, just when the printing of this volume was nearing its completion" [3]

Voevodsky too, upon finding himself in the same position as Frege, reacted with a super-human level of integrity and intellectual honesty:

In 1998, the American mathematician Carlos Simpson published a paper indicating there might be a mistake in Voevodsky and Kapranov’s 1990 result. For years Voevodsky sifted through the details without making much progress. He remained convinced the result was right. Then, in the autumn of 2013, as the leaves changed color and summer gave way to autumn, he made a breakthrough. Of sorts. He confirmed the error. The important result was no longer quite so important.

“It is plainly wrong. The main theorem is incorrect,” he says. “It’s not that there is some gap in the proof. It’s that the main theorem is plainly wrong.” The mistake, he explains, was in failing to question the obvious. “We had proved that an assertion was indeed true in all of the difficult cases, but it turned out to be false in the simple case. We never bothered to check.” In confirming the error, he added an addendum to the original citation in his official publications list—“Warning: The main theorem of this paper was shown by Carlos Simpson to be false.” [1]

It is all the more remarkable that he spent years of working through painstaking details to prove to himself that he was wrong. And rather than quietly issuing a retraction, he shouted it from the rooftops, leading a heroic charge to get mathematicians to stop hand-waving with English-language proofs, and start writing code. [4]

And I now do my mathematics with a proof assistant. I have a lot of wishes in terms of getting this proof assistant to work better, but at least I don’t have to go home and worry about having made a mistake in my work. I know that if I did something, I did it, and I don’t have to come back to it nor do I have to worry about my arguments being too complicated or about how to convince others that my arguments are correct. I can just trust the computer. There are many people in computer science who are contributing to our program, but most mathematicians still don’t believe that it is a good idea. And I think that is very wrong.[5]

1. https://nautil.us/issue/24/error/in-mathematics-mistakes-are...

2. https://plato.stanford.edu/entries/russell-paradox/

3. https://en.wikipedia.org/wiki/Russell%27s_paradox#cite_note-...

4. https://www.quantamagazine.org/univalent-foundations-redefin...

5. https://www.ias.edu/sites/default/files/pdfs/publications/le...

The first casper PoC was in 2015, and PoC2 was in early 2016.[1] However, there was a pivot from the early "consensus-by-bet" to the current version, which is based on "prepare and commit" messages. I think the current one is PoC4. [2,3]

1. https://blog.ethereum.org/2016/03/05/serenity-poc2/ 2. https://github.com/ethereum/casper 3. https://github.com/ethereum/pyethereum/pull/791