pama

Perhaps you did not understand the Fermat theorem proof announcement/repo or the link. The 13 million lines did not use any external, possibly not honest libraries, as the proof eventually only used the fundamental axioms. So for the Fermat theorem formalization, no open open questions remain.

I had good luck with Kevin Lin’s tip for Astra: “Can you radically simplify the implementation?”

You jest and that is OK. Brute force search is not something you can do over math problems of that difficulty or anything with combinatorial complexity.

To me it feels closer to taking the top 10k human mathematicians on a large retreat for a year and having them self organize to collectively solve this problem—not kids and easter eggs.

As far as I understand the 10k agents worked on the proof. The lean formalization came later and was easier/faster than getting the proof.

If you work with distributed systems, you still call that scenario a success. On the other hand, if the 3/4 of agents going off the rails bring down the whole mission, that is a failure. The latter would have been my guess with current models scaling to 10k agents.

I am not an expert in lean4, but I could follow parts of the high level lean definitions of the problem statement in the repo. A lean bug would be a fun scenario; I am certain this proof will receive the deserved scrutiny, and if it uncovers a bug, it will make the story even more exciting. It is extremely unlikely to be the case, however, because the 10k agents working on the proof didnt use lean, so it would have to be a math logic error that translates to a lean bug—perhaps something the agents picked up during training?

I am not sure what you mean here. There exist plenty high-concern biological threats that dont need any AI help. Human oncovirus design is low on my concern list (immunity is diverse), and in any case it does not need AI—rather labspace. Disgruntled high schoolers or undergrad chemists can do way more damage from readily available materials without AI and without research delay. As can nature (or amateur biologists without AI) by mixing bats with their animal of choice and waiting a while. If/when any scary global events like covid happen again, I sure hope we have true superintelligence to help us navigate it quickly.

Other than the undeniable breakthrough in math, the important point is the ability to orchestrate 10k agents to productively work on a single problem, which creates options:

> OpenAI, meanwhile, says its experience with Navier-Stokes could open the door to solving puzzles with more practical relevance. “We are now able to spend millions of dollars on a problem that we really care about and that really matters: developing new materials, finding cures to diseases,” Bubeck said. “All of those things that we have been talking about for a long time—now they seem to be at our fingertips.”

They managed to solve a problem that was beyond current human ability.

Not only that, but it used 10k agents coherently over 88 hours to come up with the proof. This is a significant advance.

So at 3 million different files you have a 98.3% chance of a hash collision. Wouldnt that cause problems in real datasets?

30 years late, but I will take it. Contracts look useful and less messy than exceptions.

Oh, the use of “load-bearing” is a pretty clean bug in the system context of Claude code. It can be fixed trivially. The overuse of particular language constructs, including the one you suggested, is a more interesting problem; it is fixable, but might involve considerably more effort.

Interesting use of Claude’s construct! Your phrasing might also suggest that it resolves something else, which is left ambiguous, whereas your other construct would be less likely to suggest that idea (unless you explicitly appended a contrastive clause for emphasis).

The bots are subtle. From your example in your GP comment (and in part depending on the surrounding context) I would expect that an empty list would be less likely the subject of: “the list contains no string”, than in “the list doesn’t contain strings”.

I might be over interpreting the intentionality of Claude in using this construct, however, these models were pretrained by reading so much more than any human, they learn to handle language differently than most humans.

> "It <verb>s no <noun>" instead of "It doesn't <verb> <noun>"

The meaning is often different in these constructs. Consider: “Claude answers no questions” vs “Claude doesn’t answer questions”. The first could be a bot or a politician avoiding the substance, the second could be a broken UI or a politician cancelling the QA of a press conference.

> Is the energy usage so different between local and cloud inference?

In throughput mode for agentic loads, the energy usage (tok/s/MW) of the new NVidia Vera Rubin hardware is 30x lower than that of the B300 and perhaps 450x lower then the H200 was, which in turn is hundreds of times lower than the inference for single users at home in any non-data-center hardware. It feels like comparing the momentum of an ant to the momentum of an elephant.

> I'm kind of lost on what to do with it.

Personal assistant (e.g. openclaw) in the mac ecosystem. You need external models to power it ofc, but cool to have all the Apple integration and local network in your assistant. The claw can be addressed in multiple ways and can command your local hardware if you so wish.

Without doubt, dsv4-flash-0731. Original weights; needs two connected DGX.

Thanks! I hadn't tried it. I've started using it today; I limited a couple options about dired-local and images in kitty due to concerns from upstream security audits, but otherwise looks fantastic.

Thanks! Agreed ghostel looks fantastic. I still wish there was an in between a full TUI and a full non-interactive version, but switching to ghostel means I can fully live within emacs again.

Similar story here (user since early 90s). I wish more AI harnesses could also have a dumb-terminal mode in addition to the fully non-interactove mode, so they could all stay naturally searchable/copyable in simple comint buffers. Even the best current terminal emulators within Emacs are not great to recursively handle Emacs (or modern AI TUI) well enough, so I occasionally also use a shell putside Emacs.

Another reason why Lockdown mode on iOS is your friend.

Hmm. I didn’t get that impression from a quick skim. Just curious: what makes you think that?

Lower latency, but broader readout of the tick bacteria at: https://nyticks.org/tick-submission/

As mentioned in the article, this is not a safe way to assess Lyme disease. I still want to know what biohazards these tiny critters hold.

Thanks

You now fully support version 1.0. IIRC, the first version of Mathematica I used back in early 1993 was 2.1 soon followed by 2.2, which was useful for a couple of years. How much extra work is it to reach full compatibility with that version? (I had used MathLink at the time.)

Application error: a client-side exception has occurred (see the browser console for more information).

iPhone; Safari; Lockdown mode.

Alzheimers has a very long development stage compared to almost all other dementia (Lewis body also has a long timeline, but none of the other forms has anywhere close to the known length for Alzheimer’s disease). The original study article has no causal analysis, so a simple explanation is that super early Alzheimers symptoms (possibly even undetectable ones outside the context of intense taxi driving) drives people to abandon their taxi- or ambulance-driving jobs and seek other forms of employment.

No secrets—all published. Very efficient attention. Excellent kernels. Great caching subsystem. Small and well trained model.

Google’s trajectory unfortunately starts to feel similar to when yahoo lost everything in the early dotcom bubble except it owned a huge chunk of Alibaba. Google’s internal decision to stop publishing useful research probably started the slow but sure process of internal decline. I still hope they can recover, given their amazing position in terms of data and infrastructure, but it no longer feels like an obvious or easy task, when only 6 or 7 years ago they felt untouchable.

Large groups suffer communication bottlenecks, so by Amdahl’s law will only be as fast as a smaller group.

You can of course have many independent small groups, but this is trivial and best left unsaid in the context of this comparison.