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
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.
@pozorvlak heh, was going to ask who Alex Honnold of this metaphor would be