Login
You're viewing the f.duriansoftware.com public feed.
  • 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

Replies

  • 💬 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