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

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://mastodon.social/@carapace/117209902491946768

Dang, that is a lot of hush money.

RE: https://dmv.community/@jcrabapple/117096943984383081

Clearly the tiny people have antimemetic powers, and the mushroom contains a powerful mnestic.

A quotation from Voltaire

Had there been a literary censorship in Rome, we should have had to-day neither Horace, Juvenal, nor the philosophical works of Cicero. If Milton, Dryden, Pope, and Locke had not been free, England would have had neither poets nor philosophers; there is something positively Turkish in proscribing printing; and hampering it is proscription.
 
[S’il y avait eu une inquisition littéraire à Rome, nous n’aurions aujourd’hui ni Horace, ni Juvénal, ni les œuvres philosophiques de Cicéron. Si Milton, Dryden, Pope, et Locke, n’avaient pas été libres l’Angleterre n’aurait eu ni des poètes, ni des philosophes: il y a je ne sais quoi de turc à proscrire l’imprimerie, et c’est la proscrire que la trop gêner.]

Voltaire (1694-1778) French writer [pseud. of Francois-Marie Arouet]
Letter (1733-06-20) to a First Commissioner [Lettre á un premier commis] [tr. Tallentyre (1919)]

More about this quote: wist.info/voltaire/85406/

#quote #quotes #quotation #qotd #voltaire #authors #censorship #classics #freepress #freedomofthepress #history #literature #perspective

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

Alas, he didn't do so well on the Greek mythology questions. I bet his mum will be giving him an earful for that. #UniversityChallenge

(Not really, I bet she is deservedly proud of him!)

@CommonMugwort

Glad that @CommonMugwort Jr got the Greek-language question, that could have been embarrassing. #UniversityChallenge

Saw two more good #edfringe shows today, both at C Aquila (the Roman Eagle Lodge, at the top of the Royal Mile):

Cowards! https://www.edfringe.com/tickets/whats-on/cowards Two-hander play about a pair of flatmates whose cowardice causes them both to screw up their relationships. Lots of fourth-wall breaking and playing with levels of reality, the kind of thing the Fringe does best. As one character says, "everyone thinks they're Fleabag". 2pm.

Emoji: The Hieroglyphs of our Time, or How I Learned to Stop Worrying and Send the Risky Text https://www.edfringe.com/tickets/whats-on/emoji-the-hieroglyphs-of-our-time-or-how-i-learned-to-stop-worrying-and-send-the-risky-text Standup act, only loosely about emoji. Several songs, and *damn* does she have a good voice. As her tech person said after the show "when all the kids sat down, I thought 'are they going to be OK with how much your tits are like, characters in the show?'". 3pm.

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

Edinburgh Fringe 2027 show idea: "Monsanto: the Pantomime".

SHELL OIL,1970s

Bespectacled science guy: I'm afraid our data is inconvertible, sir: our products are dangerously changing Earth's climate.
CEO: Oh no, this is terrible. What should we do?
Self-appointed marketing experts: Terribly *awesome*, you mean! As of right now, we're going to re-orient our entire marketing strategy around this. "Shell: changing the climate, one journey at a time". Every time global mean temperature goes up a tenth of a degree, we throw a party. Brag about how our products emit more carbon than Brand X. This is gonna be great.
BSG: ...why?
SAMEs: Because saying that we're changing the planet makes us sound powerful, which will make people want to associate themselves with us, which will make them buy our products.
BSG: Are you actually on drugs right now?
SAMEs: No, just the Power of Marketing!

2/?

I'm wondering how the "AI hacking stories are just marketing stunts, you fool, you rube" crowd would have approached some historical marketing problems.

TROY, 1184 BC

Odysseus: We wait until the Trojans drag the horse into the city, and then we burst out...
Self-appointed marketing experts: Hmmmm, yeah, love it, but I have just one note.
Odysseus: Oh?
SAMEs: You should put a banner over the horse reading "I'M FULL OF GREEKS".
Odysseus: What!?
SAMEs: And maybe occasionally let out some threatening shouts from inside, "We're gonna kill you all and burn down your city" kinda stuff. Maybe poke a sword out occasionally.
Odysseus: ...why?
SAMEs: It makes you sound powerful and dangerous. People like powerful and dangerous things.
Odysseus: And why would that make them more likely to drag the horse inside the city?
SAMEs: *tap heads knowingly* Marketing!

1/?

Does anyone know the status of the effort to formalise the proof of the classification of finite simple groups? Gonthier doesn't seem to have published anything about it since formalising the Odd-Order Theorem in 2013.

"I never thought the greenhouse gases would change MY climate!" sobs woman who voted for the Greenhouse Gases Changing People's Climate Party.

> On June 11th Mark Warner, the vice-chair of the Senate Intelligence Committee, said that General Joshua Rudd, who leads the National Security Agency and the Pentagon’s Cyber Command, had told him that Mythos “broke into almost all of our classified systems, not in weeks, but in hours”.

https://archive.is/emIoA

TENET is to particle physics what INTERSTELLAR is to general relativity or THE ODYSSEY is to Bronze Age archaeology (or ARCADIA is to chaos theory): it plays around with some ideas from a real academic discipline, in a spectacular and narratively compelling but non-rigorous way.

Rewatched SOME LIKE IT HOT at the cinema, then came home, thought "maybe I'll watch a few minutes of TENET", and of course ended up watching the whole thing. Both are great, and TENET is not nearly as hard to follow as people say, provided you pay attention. Also, it may not have a time heist, but it has a time commando raid, which is the next best thing.