Login
You're viewing the dmv.community public feed.
  • Pozorvlakpozorvlak@mathstodon.xyz
    Oct 14, 2026, 11:11 AM

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

    💬 1🔄 5⭐ 3

Replies

  • Pozorvlakpozorvlak@mathstodon.xyz
    Oct 14, 2026, 11:51 AM

    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.

    💬 1🔄 1⭐ 8
  • Pozorvlakpozorvlak@mathstodon.xyz
    Oct 14, 2026, 12:02 PM

    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).

    💬 1🔄 0⭐ 5
  • 💬 1🔄 1⭐ 1
  • Pozorvlakpozorvlak@mathstodon.xyz
    Oct 14, 2026, 1:31 PM

    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.

    💬 1🔄 3⭐ 2
  • 💬 0🔄 1⭐ 1