imranq

Everyone saying you could replace Jev or decision type models with an LLM with bolted schema output constraining are missing the point completely. Its about extreme speed and cost effectiveness with high quality, neither of which you are going to get with LLMs even with these KV-cache tricks

The main reason to learn something is actually being able to communicate in the language of that subject. There are complex ideas in math that cannot be easily captured by the language of other fields. Pepole who don't study math cannot even understand what a worthwhile goal in math even is or how it could be useful to other fields.

You can't simply prompt a model to be "better" when "better" isnt even properly defined

This guy just seems a bit salty

> Officials said some users expected Maven to flag stale records or contradictions in the intelligence assembled for potential targets, though it is not clear why they thought the system would do that

This is what happens when people who don't understand AI and its limitations embrace it wholeheartedly, thinking it's going to behave like The ultimate analyst. Except it's not. Its got blind spots in more places than anyone knows. And not to mention the system itself has multiple areas of failure.

Based on my admittedly limited research, it seems like you should use Laya for much more deterministic tasks where you have some training data. It won't be as good as Jev for zero shot cases.

Note that this proof while impressive does not add any value to mathematics as a human pursuit. But it does show we can throw these LLM beasts at much gnarlier problems than we could have imagined previously. Maybe even formally verify papers the day they are posted?

I'd love to see an e2e compiler or OS kernel verification or Full-stack chip design with formal equivalence checking at each stage that would be pretty cool.

What else is interesting is how they staged this problem : (a) maintain an explicit DAG/roadmap of sub-goals rather than one flat prompt, (b) separate statements from proofs so many agents can work on different nodes without stepping on each other, (c) keep a natural-language index alongside the formal one so search/reuse works... I feel like this is the future of long horizon agents and how you can do work that's making the most of every agent. This approach will likely be baked into the next versions of coding harnesses

Transcribed letter (from chatgpt):

Dear Mr.,

In your letter of December 14, you ask me whether mathematics is a worthwhile endeavor. Mathematics absolutely is not a worthwhile endeavor! I can imagine only three possible reasons for studying mathematics:

(1) Entertainment. (2) To promote technological progress. (3) To promote one’s own career.

Reason (1) is harmless; but one doesn’t refer to entertainment as a “worthwhile endeavor”; it’s just a pastime.

As for reason (2), modern technology is the worst thing that ever happened to the world, and to promote its progress is nothing short of criminal. Read Our Final Century, by Martin Rees; or read “Why the Future Doesn’t Need Us,” an article by Bill Joy that appeared in Wired magazine, April, 2000.

As for reason (3), to choose mathematics as one’s career would be very risky. Not long ago I received a letter from a gravestone sculptor whose craft had been rendered obsolete by a laser-guided machine that carved gravestones automatically. He was in his forties, unable to find work, and depressed. Maybe you think that can’t happen to you if you become a mathematician. But you’re wrong. Martin Rees, Bill Joy, and many other distinguished experts believe that within a few decades machines will be developed that will be more intelligent than even the smartest human beings. When that happens, people will be obsolete; they will be phased out and will be replaced by computers and robots. This will happen to everyone eventually, but mathematicians probably will become obsolete before anyone else does, because mathematics is more amenable to computerization than any other field. Hence, computers probably will surpass humans in mathematics before they do so in other areas.

Sincerely yours, Ted Kaczynski

Personally, I found that people are impressed with AI for subjects they simply don't understand, and when an expert works with AI, they're often underwhelmed. So while we're seeing some mathematics being automated and proved, I think there's a long way to go before we automate proofs with meaningful human value.

Google doesnt even use its own Go build system internally. Its all blaze / bazel, so they are not even taking advantage of the so called compiler feedback of Go. Also if languages are to be designed for agents not humans, its not clear whether the verbosity of Go will help agents at all

I think it might be 2020 when the M1 was released since I remember i had bought a mac book in 2019 and it was still intel

I really like Clawdbots safety gloves off approach - no handholding or just saying yes to every permission.

I set it up on a old macbook pro I had that had a broken screen and it works great. Now I just message my server using telegram and it does research for me, organizes my notes, and builds small apps on the fly to help with learning.

However security is a real concern. I need to understand how to create a comprehensive set of allowlists before expanding into anything more serious like bill payments or messaging people / etc