conv.

All stories
ScienceQuiet 12d · day 12

Researchers warn mechanized proofs may not survive technological change

A new paper raises concerns about the long-term preservation of mathematical knowledge encoded in interactive theorem provers.

newest coverage 11d agosummary written 11d ago3 pieces11 likes & upvotes1 comments MastodonLobstersHacker News

What to know

  • Interactive theorem provers are widely used to create mechanized proofs that encode mathematical knowledge, but this software-based approach makes them vulnerable to obsolescence.
  • Researchers identify a tension between proofs as "convincing" artifacts (for verification) versus "explaining" knowledge (for understanding and preservation across time).
  • The work raises questions about how to archive mechanized mathematics so that future generations can reproduce and access this growing body of formal mathematical work.

chrisamaphone (author) Researcher, Northeastern University

How it unfolded 2 developments, newest first · click a bar or a number to jump posts

Peak 1 piece in 3h at Sep 11, 8 PM; 3 pieces over 12 days (3 posts) Sep 11, 8 PM — 1 piece · 1 post — Mastodon 1Sep 11, 11 PM — quietSep 12, 2 AM — quietSep 12, 5 AM — quietSep 12, 8 AM — quietSep 12, 11 AM — 1 piece · 1 post — Lobsters 1Sep 12, 2 PM — 1 piece · 1 post — Hacker News 1Sep 12, 5 PM — quietSep 12, 8 PM — quietSep 12, 11 PM — quietSep 13, 2 AM — quietSep 13, 5 AM — quietSep 13, 8 AM — quietSep 13, 11 AM — quietSep 13, 2 PM — quietSep 13, 5 PM — quietSep 13, 8 PM — quietSep 13, 11 PM — quietSep 14, 2 AM — quietSep 14, 5 AM — quietSep 14, 8 AM — quietSep 14, 11 AM — quietSep 14, 2 PM — quietSep 14, 5 PM — quietSep 14, 8 PM — quietSep 14, 11 PM — quietSep 15, 2 AM — quietSep 15, 5 AM — quietSep 15, 8 AM — quietSep 15, 11 AM — quietSep 15, 2 PM — quietSep 15, 5 PM — quietSep 15, 8 PM — quietSep 15, 11 PM — quietSep 16, 2 AM — quietSep 16, 5 AM — quietSep 16, 8 AM — quietSep 16, 11 AM — quietSep 16, 2 PM — quietSep 16, 5 PM — quietSep 16, 8 PM — quietSep 16, 11 PM — quietSep 17, 2 AM — quietSep 17, 5 AM — quietSep 17, 8 AM — quietSep 17, 11 AM — quietSep 17, 2 PM — quietSep 17, 5 PM — quietSep 17, 8 PM — quietSep 17, 11 PM — quietSep 18, 2 AM — quietSep 18, 5 AM — quietSep 18, 8 AM — quietSep 18, 11 AM — quietSep 18, 2 PM — quietSep 18, 5 PM — quietSep 18, 8 PM — quietSep 18, 11 PM — quietSep 19, 2 AM — quietSep 19, 5 AM — quietSep 19, 8 AM — quietSep 19, 11 AM — quietSep 19, 2 PM — quietSep 19, 5 PM — quietSep 19, 8 PM — quietSep 19, 11 PM — quietSep 20, 2 AM — quietSep 20, 5 AM — quietSep 20, 8 AM — quietSep 20, 11 AM — quietSep 20, 2 PM — quietSep 20, 5 PM — quietSep 20, 8 PM — quietSep 20, 11 PM — quietSep 21, 2 AM — quietSep 21, 5 AM — quietSep 21, 8 AM — quietSep 21, 11 AM — quietSep 21, 2 PM — quietSep 21, 5 PM — quietSep 21, 8 PM — quietSep 21, 11 PM — quietSep 22, 2 AM — quietSep 22, 5 AM — quietSep 22, 8 AM — quietSep 22, 11 AM — quietSep 22, 2 PM — quietSep 22, 5 PM — quietSep 22, 8 PM — quietSep 22, 11 PM — quietYesterday, 2 AM — quietYesterday, 5 AM — quietYesterday, 8 AM — quietYesterday, 11 AM — quietYesterday, 2 PM — quietYesterday, 5 PM — quietYesterday, 8 PM — quietYesterday, 11 PM — quietToday, 2 AM — quietToday, 5 AM — quiet 12
Sep 12Sep 13Sep 14Sep 15Sep 16Sep 17Sep 18Sep 19Sep 20Sep 21Sep 22now · 7:45 AM ET
  1. 2

    Researchers publish paper on mechanized proof longevity

    A paper titled "Is truth futureproof? On the possible futures of mechanized proofs" was published, examining how interactive theorem provers create mechanized proofs that risk degradation over time as software ages, potentially hindering reproduction of mathematical knowledge.

    “Interactive theorem provers play increasingly important roles in the programming languages and mathematics communities, resulting in a large body of mechanized proofs that bear witness to mathematical knowledge.”
    — Paper abstract · source
  2. 1

    Lead author highlights proof preservation framework

    One of the paper's authors promoted the work on Mastodon, emphasizing the distinction between "convincing" and "explaining" modes of proof use, framing the work as addressing both proof longevity and contemporary questions about mechanized mathematics.

    “in light of recent mechanized math news, i want to re-promote the paper my colleagues and i published earlier this year about the nature of mathematical knowledge represented by mechanized proofs…”
    — chrisamaphone@hci.social
    • chrisamaphone@hci.social

      in light of recent mechanized math news, i want to re-promote the paper my colleagues and i published earlier this year about the nature of mathematical knowledge represented by mechanized proofs: https:// khoury.northeastern.edu/~cmart ens/papers/plateau26-itfp.pdf especially the "convincing" and "explaining" distinction between modes of use. our…

      chrisamaphone@hci.socialMastodon12d ago5▲view on Mastodon ↗