Achievements of Artificial Intelligence (AI)

[ScoutB]

They have LEAN to help them, a maths programming language of sorts that essentially allows them to check if the logic is correct.

Yeah exactly. Mathematicians have been happily developing Lean for the last decade intending to use it on the sort of math problem where the solution would be extremely long and tedious for humans to check manually. Turns out automatic correctness checking was exactly what AI needs.

It sounds like as @EndME says basically this person had Claude write the proof in Lean:

The Lean sources in this repository — definitions, statements and proofs, together with Challenge.lean, Solution.lean and the metadata — were written by an AI system (Anthropic's Claude models) working autonomously under the direction of Justin Leder; no human wrote or edited the Lean code. Correctness rests on mechanical checking [...] The work has not yet been refereed by human mathematicians or by anyone independent of the author; the only review so far was carried out by AI systems (adversarial reads of the formal statements and of the proof chain against the cited literature). Mechanical checking does not cover whether the formal statements express the intended mathematics: readers should satisfy themselves that the definitions in Challenge.lean state "θ(p_c) = 0 for nearest-neighbour Bernoulli bond percolation on ℤ^d, d ≥ 2".

 

[EndME]

I kind of agree but also it seems to me that if a PhD’s career can be nuked because a problem they were working on is solved. That sounds more like a problem with how the field works career wise that LLMs have exposed, than something inherently bad about LLMs. So I found it hard to completely agree with his analysis. It also seemed very melancholic.

I see your point, but I think it touches upon a larger issue: We build understanding by countless hours spent learning. It's becoming much harder to do that, because we often take shortcuts when we are offered them.

 

[ScoutB]

Part of the emphasis on new PhD's might be because established mathematicians will have tenure and be relatively safe from the immediate effects of this. There's a big pre-tenure post-tenure gap where math people are working their butt off to solve problems and get publications out beforehand, and then after they can coast more. It's rather hard for the university to get rid of them even if they're not doing anything 'useful' (and nobody knows what pure mathematicians are doing anyway). At least that's how it is in the US and Canada.

 

[EndME]

Part of the emphasis on new PhD's might be because established mathematicians will have tenure and be relatively safe from the immediate effects of this. There's a big pre-tenure post-tenure gap where math people are working their butt off to solve problems and get publications out beforehand, and then after they can coast more. It's rather hard for the university to get rid of them even if they're not doing anything 'useful' (and nobody knows what pure mathematicians are doing anyway). At least that's how it is in the US and Canada.

And who will they look up to when the new Riemann, Fermat and Gauß are ChatGPT 10.8 and Claude 14.4 with the fanciest results called theorem 12882 version 4.768?

 

[ChronicallyOverIt]

Verifiable domains will be first and will accelerate other domains. How much of biology is verifiable right now with our current knowledge is a bit unknown. I do see running tests for biology in wet labs about to make astronomic gains, making verification faster.

Think of this as chat-gpt3 and in three years Claude will be very very good at executing experiments autonomously:

 

[Yann04]

I see your point, but I think it touches upon a larger issue: We build understanding by countless hours spent learning. It's becoming much harder to do that, because we often take shortcuts when we are offered them.

I mean sure. But also like even though calculators/computer arithmetic sort of removed a whole part of “intuition” learning and grind that was deemed necessary in the past, it unlocked things we could never have imagined and propelled human knowledge much further. For the people who built a career doing and gaining intuition about what has been automated away it’s obviously very difficult at first. But it frees up very limited funding and work time to push knowledge further by focusing on what we haven’t automated away.

 

[EndME]

For the people who built a career doing and gaining intuition about what has been automated away it’s obviously very difficult at first. But it frees up very limited funding and work time to push knowledge further by focusing on what we haven’t automated away.

I think this is an illusion. A shoe cobbler does not all of a sudden become an AI engineer. Someone who spent his whole life doing one thing doesn't all of a sudden gain the ability to do a completely different thing. A large majority of the population, not just mathematicians, will not have jobs and if there's no solution to that then it might not matter so much that future generations can be taught to work on certain problems that haven't been automated away yet. And after all life is not just about pushing things further.

 

[Rick Sanchez]

With the rate at which AI is developing there is just no doubt in my mind that it won't speed up MECFS research progress massively. The achievements since the start of this year. I've never experienced anything like this in my life, doubt anyone else has either. GPT-Astra and even the cheap META models.

However the AI future does worry me. I have a have a hard time seeing it all ending well.

Would be the cruelest of ironies if it all goes to hell before a effective treatment is widely available

 

[nafione]

especially when most breakthroughs are the product of brute force with a chance factor.

I think that people massively overestimate how important reasoning really is here, especially when most breakthroughs are the product of brute force with a chance factor.

It takes some, but the level of reasoning that the average human, even the average scientist, is capable of is massively lower than what most people imagine is needed. A lot of it is just creative insight with a bit of an obsessive streak, and that's something AIs are already capable of. All it takes is being thorough and being able to accept when a hunch doesn't pan out, something humans massively struggle with, and has basically blocked all progress for us.

Frankly, it takes very little reasoning to be comparable to what the average researcher can do, and that's before you factor being able to work for millions of years subjective-equivalent-time. And AIs will be better at this by year's end anyway.

Hard disagree on your beliefs about the importance of reasoning versus progress.

It’s true that blind luck can yield discoveries, but it’s not efficient. No better than biological evolution and if we can’t do any better than that, we aren’t as smart as we think we are.

I never tracked the exact number of patents I’m named on, but it’s around 5. On two I was the sole inventor. I didn’t build 1000 prototypes like Edison, I reasoned out a solution and within a couple prototypes advanced the state of the art of a highly technical field, repeatedly. Over $100m of those products sold to date.

I’d like to think my reasoning skills are proven, I know what good reasoning is when I see it, and I understand the benefits of good reasoning. Frankly, I wish I saw more reasoning in me/cfs research because too much of it is blindly throwing darts at a board with little chance of progress, but what do I know.

As far as consumer facing LLM’s, I recognize no evidence of reasoning or intelligence in their output. Their noise isn’t useful either, it just increases the amount of slop for people to filter through. And they are worthless for filtering their own slop because they lack reasoning in the first place. Perhaps they are good for rote tasks, but they are truly bullshit machines as far as advancing the state of the art.

I think we should be very careful putting much hope in that particular tech. It could be a harmful distraction.

Machine learning in general may have its uses but I don’t think that’s what anybody is talking about when they say AI.

 

[ChronicallyOverIt]

How Claude is accelerating protein design and analytical chemistry

In this post, we share two results that show how Claude can help life scientists increase the pace of their research. In the first, we tested Claude’s ability to design protein binders from scratch, a key step in creating protein-based drugs that has historically taken a specialist weeks or...

www.anthropic.com

From a computer science prospective I find it interesting the rest of the world finds these so useless. It’s absolutely transformative, even the most staunch anti AI people are using these to program now, the tide has truly flipped in CS. The entire robotics industry is accelerating at rates that would have been unbelievable even 6 months ago. The speed at which you can develop is insane. The human is absolutely still the architect but that role has shrunken more and more.

While nothing novel was discovered here the speed at which prototype to lab will explode.

 

[mariovitali]

I suspect they use multiple LLM AI agents when working on such complex problems, with some AIs coordinating tasks and others trying out different options and possibilities.

So in a sense it doesn't matter that some AI answers are really stupid, they are probably reviewed by other AI bots and ignored. But when some of tried approaches are interesting or lead to some progress, they are explored further etc. So I suspect it's mostly the combination of large computing power and math being a self-contained system that can be reviewed by AIs as being correct or not, that allows them to solve problems like this.

I'm just guessing though, haven't read article about the new proof yet, but this is how I suspect this would work. Anyone knows more?

This is exactly the method I have been using to research ME/CFS for the past year. It is called using LLM Committee or multi-reasoning LLM analysis. We use several LLMs looking at the same problem and essentially checking each other for validity and also ranking each other. Very frequently I see examples where all LLMs agree that a particular reasoning is superior than all others.

An example is shown here however a lot of things have progressed since then :

https://s4me.info/threads/list-of-c...r-follow-up-after-decodeme.45703/#post-634489

 

[Utsikt]

It’s true that blind luck can yield discoveries, but it’s not efficient. No better than biological evolution and if we can’t do any better than that, we aren’t as smart as we think we are.

AI doesn’t care about «efficient» because it has virtually endless resources. Humans do not.

And as the world of chess has demonstrated, AI performs far better than anything humans were able to code on their own. Players are now learning from AI by trying to figure out why on earth they did pawn to H4 at that point in the game. They can also learn by using various techniques within the field of explainable AI (XAI) to figure out why AI got the result it did.

The problem AI still faces is that real life if very very complex. Mathematics or chess are relatively narrow problems in comparison. But that doesn’t mean that more advanced algorithms and increased computing power won’t eventually be able to figure out harder real life problems as well, or that it can at least outperform humans that by no means make perfect decisions.

 

[ME/CFS Science Blog]

For a group of people that prides itself in solving complex problems, it's remarkable that mathematicians have not even been able to discuss the future of their whole disciple at great depth.

Feel free to share more insight from the mathematics community because it feels like insight/warning about what's going to happen in many other fields. The coding community is similarly affected but it has many people wanting to hype AI because of commercial interests, so I feel like the mathematicians give a more authentic account of what's happening.

Was listening to this talk by Terence Tao

 

[Utsikt]

Feel free to share more insight from the mathematics community because it feels like insight/warning about what's going to happen in many other fields. The coding community is similarly affected but it has many people wanting to hype AI because of commercial interests, so I feel like the mathematicians give a more authentic account of what's happening.

Coding vs maths kind of illustrates my point above. If your goal is to make one application or hack one organisation, AI will perform well in terms of getting it done. It’s also good a brute forcing looking for vulnerabilities. This is more like maths. If your goal is to integrate many pieces of code into a much larger infrastructure in a complex organisation while getting all vitals things right, it currently struggles. This is more like real life for most people.

 

[ME/CFS Science Blog]

If your goal is to integrate many pieces of code into a much larger infrastructure in a complex organisation while getting all vitals things right, it currently struggles.

I'm not so sure, suspect we're almost at the point where AI (the top models like Claude Fable or GPT-6-Astra) is better and faster at coding than almost all human coders. I don't have a coding background though, so perhaps others can provide more insight.

It seems to have already have made an impact on students choosing computer science less at university.

 

[Utsikt]

I'm not so sure, suspect we're almost at the point where AI (the top models like Claude Fable or GPT-6-Astra) is better and faster at coding than almost all human coders. I don't have a coding background though, so perhaps others can provide more insight.

It seems to have already have made an impact on students choosing computer science less at university.
View attachment 34098

Students go where they think they will get jobs in the future. They are not going to pick a field where there are already layoffs, regardless of the reason for the layoffs. Especially not in the US with no free education, poor welfare benefits and few employee rights. But as far as I can tell, most of those layoffs have been by companies claiming it’s going to save them money, even though at least 80-90 % of all AI business projects have failed to demonstrate profitability.

If you also consider the cost of using AI to code, and that nobody are actually paying anywhere near the real costs yet because the AI companies have had virtually unlimited access to cash for a while so they subsidie it to gain customers, and that the tech companies are hiding their ballooning debts in other companies, it’s not at all clear that AI will be a better solution for a business anytime soon. Sure, you can pay many times the price of hiring coders to get it done sooner, but does that time save really matter for most regular businesses? And is it worth the price?

We’re also at a point where the access to hardware is becoming a bottleneck, and even access to energy will become problematic in the not too distant future if the exponential growth in demand continues.

 

[mariovitali]

Regarding the impact on coding and AI. I happen to have a Computer Science background and I have previously worked in software development. For this reason, I happen to know quite a few people holding managerial positions in Software houses.

The situation is as follows : They used to have teams of 20 developers (including a senior one or two senior ones) which is now down to roughly 2 developers and a senior one. Senior developers have not lost their jobs, but this happened with junior developers.

 

[ChronicallyOverIt]

Having worked in software and robotics still knowing many people in these fields @mariovitali is right this is exactly the field. Not only that but those few engineers left now output more than the entire previous team. None of them really code anymore. Again this change has happened in months not years, so only the most forward players will have made this change.

If your goal is to integrate many pieces of code into a much larger infrastructure in a complex organisation while getting all vitals things right, it currently struggles

Not sure if you have tried CODEX or Claude Code. These are very very different than the chatbot interfaces you access online where you copy and paste. These are called harnesses, and now you can actually build your own as well but that’s complicated.These can have context of your entire project via your file system. This statement definitely used to be the case maybe 8 months ago.

It’s also necessary to use plan mode inside these tools. The human is more the architect. Plan mode takes time, people spend 1-2hrs in plan mode before even building. However recently you have to do even less planning since they are getting so good. You can also increase the accuracy of these tools by using MCP and custom .md files to direct them to be better. There’s a whole world of “harnesses”, as you can now build your own in PI or OH MY PI. I imagine in the next few years these will all somewhat unify but right now everyone has their preferred harness.

Between using an AI with CLI local access to your entire project and plan mode it does pretty much exactly what you want even in large code complex code bases. Things will probably be even more different in 6 months, it’s wild times.

 

[ChronicallyOverIt]

If you also consider the cost of using AI to code, and that nobody are actually paying anywhere near the real costs yet because the AI companies have had virtually unlimited access to cash for a while so they subsidie it to gain customers

We’re almost to the point where the open weight Chinese models that are distilled larger models are extremely cheap. Which also could pop the AI bubble but that’s another conversation.

Check out open code it’s extremely cheap.

Heck with a Mac Mini (fully spec’d) right now you can run some insane models locally on that Mac that 1-2 years ago people would have paid top subscriptions for. In 1-2 years I wouldn’t be surprised if you could have current models running for way cheaper or even locally on your Mac mini

 

[Utsikt]

Again this change has happened in months not years, so only the most forward players will have made this change.

This statement definitely used to be the case maybe 8 months ago.

Seems like I’m out of date then! Thank you and mario for providing examples.