Pushing the analogy with climbing altogether too far, we can imagine maths splitting into the following "ethical codes":

- Free Solo: all proofs are discovered, written and checked by hand.
- Trad: proofs are discovered and written by hand, then formalised by hand in Lean/etc and machine-checked.
- Headpoint: an AI agent checks whether the result is true, then a human finds and formalises an independent proof.
- Sport: proofs are discovered and written by hand, then formalised in Lean/etc by AI and machine-checked.
- Redpoint: an AI agent checks whether the result is true, then a human finds an independent proof, then an AI formalises and machine-checks the human-written proof.
- Clean aid: a human works in concert with AI agents to find and formalise a human-intelligible proof.
- Murder of the Impossible: proofs are found and formalised entirely by AI; humans don't even try to understand the details.

This leaves scope for ethical standards (and thus human understanding!) to improve over time: a result that's established by a murder-of-the-impossible proof can later be aided clean, redpointed or headpointed.

If you're interested in more details about my trip (including photos!) see https://elvum.net/kindyk. If you're interested in the (sometimes surprising) ways exploratory mountaineering reminded me of maths research, see my 2017 MathsJam Gathering lightning talk: https://youtu.be/0bv6VovSmQ4

Based on what happened in climbing, I expect to see the following:

- Recreational mathematicians will continue to do maths "by hand" for fun, but many will use AI as a training/learning aid.
- Amateur researchers will vary in how much AI they use; using less AI to prove a result will attract greater praise.
- Industrial mathematicians will mostly use AI as much as possible, because the important thing is getting the result.
- I do not know what will happen to professional pure mathematicians. Will they become influencers, living off sponsorships or prize money from Tartaglia-style competitions? Those working in "purer" (less AI) styles might attract more praise from within the community, but less sponsorship money (because the results they obtain are less flashy).

If I ever write that essay, here's what it will say:

- Lots of people are opining about what AI means for mathematics, often using mountain-based metaphors. Most of them have not done novel work in both maths and mountaineering. I have.
- In 1971, the mountaineering world was shocked by Cesare Maestri's "Compressor Route" on Cerro Torre. Maestri drilled 300 bolts up the face, climbed them using rope ladders, and left the air-compressor hanging off the top as a "screw you" to the mountaineering community.
- Reinhold Messner responded with the essay "The Murder of the Impossible", calling for mountaineers not to "carry their courage in their rucksacks".
- This basically worked; the world's mountains are not covered with bolt ladders.
- But bolts have changed the sport, for the better. In the 1980s, bolt-protected "sport climbs" led to an explosion in technical climbing standards. In 2012, the former sport climber David Lama (RIP) made the first free ascent of the Compressor Route.
- The existence of bolts, or more powerful assistive technologies like helicopters, has not ended exploratory mountaineering. Instead, climbers choose the "ethics" of their climbs to preserve challenge. Andy (RIP) and I did our FAs "alpine style", which is one of the more demanding codes; for a harder route we might have relaxed those constraints. Repeat ascents are expected to match or improve on the ethics of the first ascent.
- Similarly, AI tools will not mean the end of human mathematics. But they will profoundly change human *professional* mathematics. Rope-access techs - who often climb recreationally - do not care about climbing "ethics" in their day jobs. If you need to inspect a summit, you do it from the air.

I Climbed Four Unclimbed Peaks In Central Asia Despite The Existence Of Helicopters; Here's What That Taught Me About The Future Of Mathematics

RE: https://mathstodon.xyz/@pozorvlak/117399523683693329

OK, gonna stick my neck out. I think there is a good chance we will see a claimed solution to Hodge and maybe BSD by the start of #BigMathsJam. I would be shocked if we saw solutions to PvNP or Riemann. I have no strong opinion on Yang-Mills.

Which of the remaining Millennium Prize problems will be (credibly claimed to be) solved by the start of #BigMathsJam on November 14th?

Update: the quality was too potatoey, so we're renting an HD version from YouTube for the princely sum of £2.99 and starting again.

#nowplaying Kandukondain Kandukondain, a Tamil-language adaptation of Sense and Sensibility from 2000. So far we have seen a helicopter land and a bunch of soldiers shooting each other in some sort of jungle. I suspect the grizzled major will turn out to be Colonel Brandon.

We're watching the potato-quality version here: https://www.youtube.com/watch?v=kdyuTjH-ze8

@svat

One of my favourite parts of "Zen and the Art of Motorcycle Maintenance" is when the narrator fixes the slipping handlebar grip on his friend's bike by shimming it with a strip of aluminium cut from a beer can. "You can't fix fifty years of German engineering excellence with a beer can!" cries his horrified friend, before going to the official BMW garage to pay through the nose for the official shim. The narrator then spends a paragraph explaining why actually, any German engineer with fifty years of experience would say that a strip of beer can was an ideal choice.

So when the handlebar grip on my bicycle started slipping, I knew exactly how to fix it. A shim made of beer can aluminium!

Reader, it did not work. At all.

As far as I can tell, the Navier-Stokes regularity problem has now been resolved in the most annoying way possible:
- we have a single counterexample, not a general theorem;
- we have no real idea how it was found, but it seems to have been existing ideas and a lot of elbow grease;
- this makes no difference in practical applications, which use finite-element numerical methods;
- there's no way to apply this to other PDEs, or to improve our understanding of turbulence;
- the possibility of being scooped by an AI company (and possibly one that's spying on its customers) will discourage people from sharing their work-in-progress on big problems.

In other words, the opposite of what the Millennium Prizes were supposed to achieve! Am I missing something?

EDIT: after a bit more reading, I don't think the situation is quite this bad. The "existing ideas" (the construction of Córdoba and Martínez-Zoroa) have also been used to construct blowups in several related PDEs, so there's an obvious follow-on question about how far they can be pushed - and they've been demonstrated to be more important than most mathematicians realised. I know even less about numerical methods than I know about fluid dynamics, but apparently the way the construction builds ever-smaller perturbations might have implications for building better subgrid models. But we've lost any insight that we might have got from the "elbow grease" phase of the construction, and the way the proof came out will cause a lot of mathematicians to be less transparent.

RE: https://eigenmagic.net/@abstractcode/117170883405316011

I agree that OpenAI and the others were reckless, both in how they carried out these experiments and in doing them at all. But they did *try* to stop the agents breaking out¹. They were just insufficiently competent and paranoid to actually stop them. And you know what? I don't think most of the people pushing the "agents didn't hack without authorisation, the people are to blame" line would be sufficiently competent or paranoid either. This was a sophisticated and tenacious attack. OpenAI's report is out now, and it makes for horrifying reading: https://openai.com/index/hugging-face-incident-and-the-road-ahead/

¹ Apart from AISI, who deliberately ran their experiments with full Internet access to see what would happen. WTF, guys.

Just don't get me started on Hillary Putnam's linguistic argument against the simulation hypothesis, which still makes me angry 27 years after I first encountered it.

I keep seeing people cite Searle's "Chinese Room" argument approvingly. This is annoying, because it's an incredibly dumb argument that relies on

- sleight-of-hand between the program and the CPU executing it
- overindexing on the details of 1950s machine-translation efforts
- ignorance of how computers actually work, and
- xenophobia.

For a longer and more detailed evisceration, please see Mark Rosenfelder's 2002 essay https://www.zompist.com/searle.html (now with 2026 update on how LLMs affect the picture! TL;DR they do not make Searle's argument look any better).

RE: https://mathstodon.xyz/@gregeganSF/117121709868547118

I think these "AI overviews" are a big reason why so many people underestimate the capabilities of modern LLMs. It's a worst-case scenario for errors and hallucinations: one-shot, small models, tight latency constraints, no oracle to validate output against. It's a total waste of time and energy. And if you're an AI refusenik, you never see them under more favourable conditions!

[I am not saying you should *like* LLMs, but I'm begging you to *take them seriously*.]

RE: https://mathstodon.xyz/@slava/117088440250923180

Maths friends! @slava thinks that the problem here is not actually hard, and someone who understands algebra well enough could figure it out with a moment's thought. Wanna have a go at beating the bot? The challenge is to determine whether the monoid

⟨a,b|abab=baa, bbbb=1⟩

is cancellative, i.e. for all 𝑥,𝑦,𝑧, does 𝑧𝑥=𝑧𝑦⇒𝑥=𝑦 and 𝑥𝑧=𝑦𝑧⇒𝑥=𝑦?

RE: https://mathstodon.xyz/@pozorvlak/117088183762779341

Why I think this matters: there's currently a lot of cope in the maths world along the lines of "well of course the models can resolve decades-old open problems for a few thousand dollars' worth of tokens, but their exposition sucks so maybe there will still be a role for human mathematicians." This is an early sign that that take will age about as well as "You can always tell if an image was AI-generated, just count the fingers."

An unreleased version of Claude found an improved lower bound for the length of the minimum superpermutation on seven symbols: https://github.com/jlebar/superperm7-ge-5898

I can't speak to the quality of the formalisation, but the exposition is *dramatically* better than those we've seen from current frontier models in the last couple of weeks.

@slava saw this and thought of you: https://gowers.wordpress.com/2026/03/20/group-and-semigroup-puzzles-and-a-possible-polymath-project/

/cc @mjd @amenonsen

I'd actually love to see a "historically accurate" movie about the Trojan War, by which I mean a movie that says "what's the closest thing to Homer's story that fits with what archaeology tells us about the period?" Mycenaean Greeks, driven to desperation by years of drought, try to capture a wealthy and strategically-located Hittite client state while the Hittite Empire is distracted by its own internal problems. A matrimonial alliance gone wrong as casus belli. Not a protracted siege, but years of seasonal attacks accompanied by raids up and down the coast to secure supplies. Trojan allies coming from the Caucasus and Sub-Saharan Africa (as described in the lost Aethiopis epic). A horse-headed treasure ship left behind as tribute, but the ship only contains a thin layer of treasure and then MURDER the rest of the way down. Greek warlords wearing boar's-tusk helmets. Scribes back home desperately trying to balance the books in Linear B.

I just don't trust Grok to make it for us.