Research ethics and attribution

Amina, a doctoral student in Nairobi, proves a lemma she needs for her thesis. A month later, reading a 1978 paper for a different reason, she finds the same lemma, with a different proof. Three collaborators — in São Paulo, Hanoi and Toronto — finish a paper: one had the key idea, one did the long computations, one wrote most of the text. In what order should their names appear? A postdoc asks an AI system to prove a technical lemma, gets a fluent proof, and then asks three other AI systems, which all say it is correct. May she state the lemma as proved?

None of these is exotic; every research mathematician meets them. Two principles organise the answers:

• Mathematical truth does not depend on who discovers it, but credit for a discovery belongs to those who made it. Citation and attribution are how the community keeps that record.
• A claim is established only when it has been proved and the proof has been checked — by people, or by a verified formal method. Everything else must be labelled for what it is: a citation, a conjecture, a heuristic, a computation.

This lesson builds on reading the mathematical literature, where you learned to classify the claims in a paper; here you learn to make your own claims, and give your own credit, honestly.

Mathematics shares the general principles of research integrity — honesty, fairness, responsibility — but three features give them a particular shape.

1. The literature is a dependency graph. A theorem rests on the results it uses, which rest on others. A citation is an edge in that graph: it says "this argument depends on that one". A missing citation hides a dependency; a false lemma infects everything downstream until it is found and the record corrected. (This is the same graph a formalisation blueprint makes explicit; see formalising published mathematics.)
2. Proofs can be checked. Unlike most empirical claims, a mathematical error can usually be identified definitively. That makes correction possible — and expected. Admitting an error costs little compared with the damage a known, uncorrected error does to everyone who relies on it.
3. Credit is the currency, and it is unevenly distributed. Hiring, grants and invitations depend on who is known to have done what. Researchers who are early in their careers, far from major centres, or from groups historically excluded from mathematics are the most easily harmed when credit is misassigned — and the history of mathematics has many such cases.

First: how an error was repaired. Cauchy's Cours d'analyse (1821) stated that if a series of functions continuous near a point converges there, its sum is continuous there. In 1826 Abel remarked that the theorem "admits exceptions", citing the series $\sin x - \tfrac12 \sin 2x + \tfrac13 \sin 3x - \cdots$, which converges for every real $x$, to $x/2$ on $(-\pi, \pi)$, and so jumps at $x = \pi$. A simpler exception:

The repair, found by Seidel and by Stokes in 1847 and made central by Weierstrass, is to strengthen the hypothesis.

Historians still discuss how Cauchy's statement should be read — his notion of convergence and of infinitely small quantities was not ours, and Imre Lakatos (1976) used the episode as a case study in how proofs and concepts evolve together. What is not in dispute is the pattern: a published claim failed, a counterexample was credited to the person who found it, and the theorem was repaired by finding the hypothesis the proof actually used. That pattern is the ethical ideal.

Second: what agreement is worth. Consider $k$ checkers — referees, programs or AI systems — who all accept a proof. Model them as follows. A correct proof is always accepted. A flawed proof is accepted by each checker with probability $q$; with probability $\rho$ the checkers share a blind spot and return one common verdict, and otherwise they judge independently. Then all $k$ accept a flawed proof with probability $\rho q + (1 - \rho) q^k$, and if the prior probability that the proof is correct is $\pi_0$, Bayes' rule gives

With $\pi_0 = \tfrac12$, $q = \tfrac35$ and $\rho = \tfrac12$ the ceiling is $\tfrac{10}{13} \approx 0.77$: a hundred agreeing checkers still leave at least a $\tfrac{3}{13}$ chance — nearly one in four — that the proof is wrong. The model is a toy — real checkers' errors are correlated in ways nobody can quantify — but its moral is robust. Agreement is evidence only to the extent that the checkers fail independently, which is precisely what cannot be assumed for AI systems with overlapping training data and similar architectures, or for referees who all skim the same hard step. And even independent agreement is evidence, not proof. This is the sense in which agreement among several AI systems is not evidence that a proof is correct: it cannot establish correctness, and because the correlation of their errors is unknown, it does not even tell you how far your confidence should move. Proofs must be checked by people or by verified formal methods.

The commonest dishonesty in mathematical writing is not fabrication but blurred status: a conjecture cited as if proved, a heuristic presented as an argument, numerical evidence described as "confirming" a statement. Some history explains why the labels matter.

• Euler's conjecture on sums of like powers (1769): at least $k$ positive $k$-th powers are needed to sum to a $k$-th power. It was believed for almost two centuries. In 1966 L. J. Lander and T. R. Parkin found, by a computer search, $27^5 + 84^5 + 110^5 + 133^5 = 144^5$; their paper in the Bulletin of the AMS is two sentences long. In 1988 Noam Elkies found infinitely many counterexamples for fourth powers, and Roger Frye found the smallest, $95800^4 + 217519^4 + 414560^4 = 422481^4$.
• Fermat numbers. Fermat believed that every $F_n = 2^{2^n} + 1$ is prime; $F_0, \dots, F_4$ are. In 1732 Euler showed that $641$ divides $F_5 = 4294967297$. No $F_n$ with $n \ge 5$ is known to be prime.
• Mersenne's list (1644) of exponents $p \le 257$ with $2^p - 1$ prime contained five errors, corrected over three centuries by Pervushin (1883), Cole (1903), Powers (1911 and 1914) and others. Cole's factorisation $2^{67} - 1 = 193707721 \times 761838257287$, presented at a meeting of the American Mathematical Society in 1903, is a famous example of a correction that needed no words.
• Overwhelming evidence can mislead. Pólya's conjecture (that for every $n \ge 2$, at least half the numbers from $1$ to $n$ have an odd number of prime factors, counted with multiplicity) holds up to $906{,}150{,}256$ and fails at $906{,}150{,}257$ (Haselgrove 1958 proved that it fails; Tanaka found the first counterexample in 1980). The Mertens conjecture was disproved by Odlyzko and te Riele (1985) without an explicit counterexample, which is believed to be astronomically large.

Arthur Jaffe and Frank Quinn (1993) argued that speculative "theoretical mathematics" should be labelled as such, so that credit goes both to those who conjecture and to those who prove; William Thurston's reply (1994) stressed that understanding and ideas also deserve credit, and that the community's norms must recognise them. Both agreed on the essential point: say what you have proved, and what you have not.

Ethics is not a formal subject: no proof assistant can decide who had an idea first, whether a source was cited, or who deserves to be an author. But several claims in this lesson are mathematical, and the Lean module checks them.

The agreement model. The definition and the two halves of the proposition:

/-- A toy model of `k` checkers (people, programs or AI systems) who all accept a proof.
A correct proof is always accepted. A flawed proof is accepted by each checker with probability
`q`; with probability `ρ` the checkers share a blind spot and give one common verdict, otherwise
they judge independently. So all `k` accept a flawed proof with probability `ρq + (1 − ρ)qᵏ`, and
by Bayes' rule the probability that the proof is correct, given `k` acceptances and prior
probability `prior`, is the value below. -/
noncomputable def posterior (prior q ρ : ℝ) (k : ℕ) : ℝ :=
  prior / (prior + (1 - prior) * (ρ * q + (1 - ρ) * q ^ k))

/-- **Correlated agreement has a ceiling.** However many checkers agree, the posterior never
exceeds `prior / (prior + (1 − prior)ρq)`: the term `(1 − ρ)qᵏ` can only shrink to zero, while the
shared blind spot `ρq` remains. -/
theorem posterior_le_ceiling {prior q ρ : ℝ} (hp₀ : 0 < prior) (hp₁ : prior ≤ 1) (hq : 0 ≤ q)
    (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) (k : ℕ) :
    posterior prior q ρ k ≤ prior / (prior + (1 - prior) * (ρ * q)) := by
  unfold posterior
  have h1 : 0 ≤ 1 - prior := by linarith
  have h2 : 0 ≤ (1 - ρ) * q ^ k := mul_nonneg (by linarith) (pow_nonneg hq k)
  apply div_le_div_of_nonneg_left hp₀.le
  · have : 0 ≤ (1 - prior) * (ρ * q) := mul_nonneg h1 (mul_nonneg hρ₀ hq)
    linarith
  · have : (1 - prior) * (ρ * q) ≤ (1 - prior) * (ρ * q + (1 - ρ) * q ^ k) :=
      mul_le_mul_of_nonneg_left (by linarith) h1
    linarith

/-- The ceiling is strictly below certainty as soon as the prior is below 1 and a shared blind
spot is possible (`ρq > 0`). -/
theorem ceiling_lt_one {prior q ρ : ℝ} (hp₀ : 0 < prior) (hp₁ : prior < 1) (hρq : 0 < ρ * q) :
    prior / (prior + (1 - prior) * (ρ * q)) < 1 := by
  have h : 0 < (1 - prior) * (ρ * q) := mul_pos (by linarith) hρq
  rw [div_lt_one (by linarith)]
  linarith

/-- By contrast, if the checkers err **independently** (`ρ = 0`) and each sometimes rejects a
flawed proof (`q < 1`), the posterior tends to `1` as the number of agreeing checkers grows,
because `qᵏ → 0`. Independence is exactly what cannot be assumed for systems with shared
training data or shared habits of thought. -/
theorem independent_tendsto_one {prior q : ℝ} (hp₀ : 0 < prior) (hq₀ : 0 ≤ q) (hq₁ : q < 1) :
    Tendsto (fun k : ℕ => posterior prior q 0 k) atTop (𝓝 1) := by
  have hpow : Tendsto (fun k : ℕ => q ^ k) atTop (𝓝 0) :=
    tendsto_pow_atTop_nhds_zero_of_lt_one hq₀ hq₁
  have hfun : (fun k : ℕ => posterior prior q 0 k) =
      fun k => prior / (prior + (1 - prior) * q ^ k) := by
    funext k
    simp [posterior]
  rw [hfun]
  have hden : Tendsto (fun k : ℕ => prior + (1 - prior) * q ^ k) atTop
      (𝓝 (prior + (1 - prior) * 0)) :=
    tendsto_const_nhds.add (tendsto_const_nhds.mul hpow)
  rw [mul_zero, add_zero] at hden
  have hlim := (tendsto_const_nhds (x := prior)).div hden hp₀.ne'
  rw [div_self hp₀.ne'] at hlim
  exact hlim

An error and its repair. The refutation of the pointwise sum theorem is proved from scratch, following the human proof; the corrected theorem is in Mathlib.

/-- **Cauchy's "sum theorem" is false as stated.** Cauchy's *Cours d'analyse* (1821) asserted that
a convergent series of continuous functions has a continuous sum; Abel (1826) pointed out an
exception. Here is a simple counterexample to the pointwise version: `fₙ(x) = c(x)ⁿ`, where
`c(x) = max 0 (min x 1)` clamps `x` to `[0, 1]`, is continuous for every `n`, but `fₙ(x)` tends to
`0` for `x < 1` and to `1` for `x ≥ 1`, a discontinuous limit (by the intermediate value
theorem, a continuous function on `ℝ` taking the values 0 and 1 also takes the value 1/2). -/
theorem cauchy_sum_theorem_false :
    ¬ ∀ (f : ℕ → ℝ → ℝ) (g : ℝ → ℝ), (∀ n, Continuous (f n)) →
      (∀ x, Tendsto (fun n => f n x) atTop (𝓝 (g x))) → Continuous g := by
  intro H
  let c : ℝ → ℝ := fun x => max 0 (min x 1)
  let g : ℝ → ℝ := fun x => if 1 ≤ x then 1 else 0
  have hcont : Continuous g := by
    refine H (fun n x => c x ^ n) g (fun n => ?_) (fun x => ?_)
    · exact (continuous_const.max (continuous_id.min continuous_const)).pow n
    · by_cases hx : 1 ≤ x
      · have hc : c x = 1 := by simp [c, min_eq_right hx]
        simp only [hc, one_pow, g, ite_eq_left hx]
        exact tendsto_const_nhds
      · have hc₀ : 0 ≤ c x := le_max_left _ _
        have hc₁ : c x < 1 := max_lt one_pos (min_lt_iff.2 (Or.inl (not_le.1 hx)))
        simp only [g, ite_eq_right hx]
        exact tendsto_pow_atTop_nhds_zero_of_lt_one hc₀ hc₁
  -- A continuous `g` with `g 0 = 0` and `g 1 = 1` takes the value `1/2`.
  obtain ⟨x, hx⟩ := intermediate_value_univ 0 1 hcont
    (show (1 / 2 : ℝ) ∈ Set.Icc (g 0) (g 1) by norm_num [g])
  simp only [g] at hx
  split_ifs at hx <;> norm_num at hx

/-- **The corrected theorem.** A *uniform* limit of continuous functions is continuous — the
hypothesis that Seidel and Stokes (1847) identified and Weierstrass made central. This is
Mathlib's `TendstoUniformly.continuous`. -/
theorem uniform_limit_continuous {f : ℕ → ℝ → ℝ} {g : ℝ → ℝ} (hf : ∀ n, Continuous (f n))
    (hu : TendstoUniformly f g atTop) : Continuous g :=
  hu.continuous (Eventually.of_forall hf).frequently

Claims in the record. Mersenne's five errors, Cole's factorisation, and the refutations of Euler's and Fermat's conjectures — each checked by Lean's kernel. The Mersenne facts apply Mathlib's formalised Lucas–Lehmer test.

/-- **Mersenne's list, corrected.** In 1644 Mersenne claimed that, for `p ≤ 257`, `2^p − 1` is
prime exactly for `p = 2, 3, 5, 7, 13, 17, 19, 31, 67, 127, 257`. He was wrong about five
exponents: `2^61 − 1`, `2^89 − 1` and `2^107 − 1` are prime, and `2^67 − 1` and `2^257 − 1` are
not. Each fact is proved by applying Mathlib's Lucas–Lehmer theorem
(`lucas_lehmer_sufficiency`, `lucas_lehmer_necessity`), with `norm_num` running the test. -/
theorem mersenne_list_corrected :
    (mersenne 61).Prime ∧ ¬ (mersenne 67).Prime ∧ (mersenne 89).Prime ∧
      (mersenne 107).Prime ∧ ¬ (mersenne 257).Prime := by
  refine ⟨lucas_lehmer_sufficiency _ (by simp) (by norm_num), fun h => ?_,
    lucas_lehmer_sufficiency _ (by simp) (by norm_num),
    lucas_lehmer_sufficiency _ (by simp) (by norm_num), fun h => ?_⟩
  · have := lucas_lehmer_necessity 67 (by norm_num) h
    norm_num at this
  · have := lucas_lehmer_necessity 257 (by norm_num) h
    norm_num at this

/-- **Cole's factorisation (1903).** Frank Nelson Cole exhibited the factors of `2^67 − 1`,
showing directly that Mersenne's `67` was wrong: `2^67 − 1 = 193707721 · 761838257287`. -/
theorem cole_factorisation : mersenne 67 = 193707721 * 761838257287 := by
  norm_num [mersenne]

/-- **Euler's conjecture on sums of like powers is false** (Lander and Parkin, 1966, found by a
computer search): Euler conjectured (1769) that at least `k` positive `k`-th powers are needed to
sum to a `k`-th power, but `27⁵ + 84⁵ + 110⁵ + 133⁵ = 144⁵`. -/
theorem euler_conjecture_false :
    ¬ ∀ a b c d e : ℕ, 0 < a → 0 < b → 0 < c → 0 < d → a ^ 5 + b ^ 5 + c ^ 5 + d ^ 5 ≠ e ^ 5 :=
  fun H => H 27 84 110 133 144 (by norm_num) (by norm_num) (by norm_num) (by norm_num)
    (by norm_num)

/-- **Fermat's conjecture on the numbers `Fₙ = 2^(2^n) + 1` is false** (Euler, 1732): Fermat
believed they are all prime, but `641` divides `F₅ = 2³² + 1 = 4294967297`. Uses Mathlib's
`Nat.fermatNumber`. -/
theorem fermat_conjecture_false : ¬ ∀ n : ℕ, (Nat.fermatNumber n).Prime := by
  intro H
  have h641 : 641 ∣ Nat.fermatNumber 5 := by norm_num [Nat.fermatNumber]
  rcases (H 5).eq_one_or_self_of_dvd 641 h641 with h | h
  · norm_num at h
  · norm_num [Nat.fermatNumber] at h

The alphabetical convention. Made precise, it says that the author list is a function of the set of authors — the order carries no information about contribution — and that sorting neither adds nor drops anyone. Formalising it exposed a hidden choice: "alphabetical" depends on a collation, and Lean's code-point order puts "Álvarez" after "Zhang".

/-- The alphabetical convention for author lists, made precise: sort the names. Lean compares
strings by Unicode code points, which is *not* the order of any dictionary — see
`author_order_example`. -/
def authorOrder (authors : List String) : List String :=
  authors.mergeSort (· ≤ ·)

/-- An alphabetical author list depends only on who the authors are: any two orderings of the
same names sort to the same list. So the order carries no information about who did what — which
is the point of the convention. (Both sorted lists are permutations of each other and sorted, and
a sorted list is determined by its elements.) -/
theorem authorOrder_eq_of_perm {l₁ l₂ : List String} (h : l₁.Perm l₂) :
    authorOrder l₁ = authorOrder l₂ :=
  List.Perm.eq_of_sortedLE List.sortedLE_mergeSort List.sortedLE_mergeSort
    (((List.mergeSort_perm l₁ _).trans h).trans (List.mergeSort_perm l₂ _).symm)

/-- Sorting neither drops nor adds an author: `a` is in the sorted list exactly when `a` is in the
original list (core Lean's `List.mergeSort_perm`). -/
theorem mem_authorOrder {authors : List String} {a : String} :
    a ∈ authorOrder authors ↔ a ∈ authors :=
  (List.mergeSort_perm authors _).mem_iff

/-- Formalising forces a hidden convention into the open: in code-point order an accented capital
comes after `Z`, so "Álvarez" sorts after "Zhang", unlike in a Spanish or English dictionary. A
journal's "alphabetical" order is a choice of collation, which must be stated. -/
theorem author_order_example :
    authorOrder ["Zhang", "Álvarez", "Okafor", "Bose"] = ["Bose", "Okafor", "Zhang", "Álvarez"] := by
  simp [authorOrder, List.mergeSort]

What is formalised, and what is not. Formalised: the model's ceiling and limit, the counterexample and the corrected theorem, five facts about Mersenne numbers, three refutations, and two properties of sorted author lists. Not formalised — and not formalisable — is everything that makes this lesson about ethics: whether a model of checkers fits reality, who discovered what, and what is fair. Note also the provenance labels: the corrected theorem and the Mersenne facts apply Mathlib's theorems, and say so; attribution matters in formal libraries too.

The first experiment evaluates the agreement model exactly, for independent and correlated checkers, and confirms the formula with a seeded simulation of the model.

"""How much does it tell you when several checkers agree?

A toy model. A proof is correct with prior probability `prior`. Each of k
checkers (people, programs or AI systems) always accepts a correct proof and
accepts a flawed proof with probability q. With probability rho the checkers
share a blind spot and return one common verdict; otherwise they judge
independently. Then all k accept a flawed proof with probability
rho*q + (1 - rho)*q^k, and Bayes' rule gives the probability that the proof is
correct after k acceptances.

We compute this exactly (with fractions) for independent checkers (rho = 0)
and correlated ones (rho = 1/2), show the ceiling that correlated agreement
can never exceed, and confirm the formula by a seeded simulation of the model.
The Lean module proves the ceiling and the limit for independent checkers.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from fractions import Fraction
import random
import textwrap

def accept_flawed(q, rho, k):
    """Probability that all k checkers accept a flawed proof."""
    return rho * q + (1 - rho) * q ** k

def posterior(prior, q, rho, k):
    """Probability that the proof is correct, given k acceptances."""
    return prior / (prior + (1 - prior) * accept_flawed(q, rho, k))

def ceiling(prior, q, rho):
    """The limit of the posterior as k grows, for 0 <= q < 1."""
    return prior / (prior + (1 - prior) * rho * q)

def simulate(prior, q, rho, k, trials, seed=2024):
    """Monte Carlo estimate of P(correct | all k accept) in the model."""
    rng = random.Random(seed)
    accepted = correct_and_accepted = 0
    for _ in range(trials):
        correct = rng.random() < prior
        if correct:
            all_accept = True
        elif rng.random() < rho:
            all_accept = rng.random() < q
        else:
            all_accept = all(rng.random() < q for _ in range(k))
        if all_accept:
            accepted += 1
            correct_and_accepted += correct
    return correct_and_accepted / accepted, accepted

def main():
    prior, q = Fraction(1, 2), Fraction(3, 5)
    print(f"Prior P(correct) = {prior}; a flawed proof fools one checker "
          f"with probability {q}")
    print()
    print("  k   independent (rho = 0)   correlated (rho = 1/2)")
    for k in [1, 2, 3, 5, 10, 20]:
        ind = posterior(prior, q, 0, k)
        cor = posterior(prior, q, Fraction(1, 2), k)
        print(f"{k:>3}   {float(ind):>21.5f}   {float(cor):>22.5f}")
    cap = ceiling(prior, q, Fraction(1, 2))
    print(f"Ceiling for rho = 1/2: {cap} = {float(cap):.5f}, never exceeded")
    print()
    estimate, n = simulate(0.5, 0.6, 0.5, 10, 40000)
    exact = float(posterior(prior, q, Fraction(1, 2), 10))
    half_width = 1.96 * (estimate * (1 - estimate) / n) ** 0.5
    print(f"Simulation, rho = 1/2, k = 10: {estimate:.4f} +/- {half_width:.4f}"
          f" from {n} accepted runs")
    print(f"Exact value from the formula:   {exact:.4f}")
    print()
    print(textwrap.fill(
        "Epistemic status: the table is exact arithmetic in a toy model and the "
        "simulation is statistical evidence that the formula describes the "
        "model. The model is an illustration, not a description of real "
        "reviewers or AI systems, whose errors are correlated in unknown ways. "
        "Its lesson is qualitative: agreement is evidence only to the extent "
        "that the checkers' errors are independent, and it is never a proof.",
        width=78,
    ))

if __name__ == "__main__":
    main()

The second reruns three centuries of corrections in a fraction of a second: the Lucas–Lehmer test for every prime $p \le 257$, compared with Mersenne's list, and the other corrections described above.

"""Checking claims in the historical record, and crediting who corrected them.

In 1644 Marin Mersenne asserted that, for exponents p up to 257, the number
2^p - 1 is prime exactly for p = 2, 3, 5, 7, 13, 17, 19, 31, 67, 127, 257. He
gave no proof, and the list was corrected piece by piece over almost three
centuries. Today the Lucas-Lehmer test settles every case in a moment.

We run the test for every prime p <= 257, compare with Mersenne's list, and
re-check three other famous corrections: Cole's factorisation of 2^67 - 1
(1903), Euler's divisor 641 of the Fermat number 2^32 + 1 (1732), and Lander
and Parkin's counterexample to Euler's conjecture on sums of like powers
(1966).

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from math import isqrt
import textwrap

#: Mersenne's claimed exponents (Cogitata Physico-Mathematica, 1644).
MERSENNE_CLAIM = [2, 3, 5, 7, 13, 17, 19, 31, 67, 127, 257]

def is_prime(n):
    """Trial-division primality test, for small n."""
    return n >= 2 and all(n % d for d in range(2, isqrt(n) + 1))

def lucas_lehmer(p):
    """Is 2^p - 1 prime? Lucas-Lehmer test for odd prime p; p = 2 directly."""
    if p == 2:
        return True
    m = (1 << p) - 1
    s = 4
    for _ in range(p - 2):
        s = (s * s - 2) % m
    return s == 0

def mersenne_exponents(limit):
    """All primes p <= limit with 2^p - 1 prime."""
    return [p for p in range(2, limit + 1) if is_prime(p) and lucas_lehmer(p)]

def compare(claimed, actual):
    """Exponents claimed but wrong, and exponents missing from the claim."""
    return sorted(set(claimed) - set(actual)), sorted(set(actual) - set(claimed))

def main():
    actual = mersenne_exponents(257)
    wrong, missing = compare(MERSENNE_CLAIM, actual)
    print(f"Primes p <= 257 tested by Lucas-Lehmer: "
          f"{sum(is_prime(p) for p in range(258))}")
    print(f"2^p - 1 is prime for p = {', '.join(map(str, actual))}")
    print(f"Mersenne (1644) claimed p = {', '.join(map(str, MERSENNE_CLAIM))}")
    print(f"   claimed but composite: {wrong}")
    print(f"   prime but omitted:     {missing}")
    print()
    a, b = 193707721, 761838257287
    print(f"Cole (1903): {a} x {b} = 2^67 - 1: {a * b == 2 ** 67 - 1}")
    f5 = 2 ** 32 + 1
    print(f"Euler (1732): 2^32 + 1 = 641 x {f5 // 641}: {f5 % 641 == 0}")
    lhs = 27 ** 5 + 84 ** 5 + 110 ** 5 + 133 ** 5
    print(f"Lander-Parkin (1966): 27^5 + 84^5 + 110^5 + 133^5 = {lhs}")
    print(f"                      144^5                         = {144 ** 5}")
    print()
    print(textwrap.fill(
        "Epistemic status: exact integer arithmetic. The Lucas-Lehmer test is a "
        "theorem (Lucas, 1878; Lehmer, 1930), so its output is a proof of "
        "primality or compositeness provided this short program is correct; the "
        "Lean module proves the same five corrections to Mersenne's list with "
        "Mathlib's formalised test. Computation cannot say who deserves credit: "
        "that is recorded in the lesson's history.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Computation is exact here, but it cannot say who deserves credit for each correction; that is a historical question, answered by the record.

The curves show the probability that a proof is correct after $k$ checkers all accept it, in the model above: correlated checkers (shared blind spot with probability $r$), independent checkers, and the ceiling for the correlated case. Move $r$ to $0$ and the correlated curve rises to certainty; move it up and the curve flattens below the ceiling. Then lower $q$ (the chance that one checker is fooled): good independent checkers help quickly, but even excellent correlated ones cannot get past the ceiling.

• Cardano and Tartaglia. In 1539 Niccolò Tartaglia gave Gerolamo Cardano his method for solving cubic equations, after Cardano swore not to publish it. When Cardano and Lodovico Ferrari learned that Scipione del Ferro had found the method earlier, Cardano published it in his Ars Magna (1545), crediting both del Ferro and Tartaglia. Tartaglia regarded this as a betrayal, and a bitter public dispute followed — an early case in which correct attribution and a broken promise pulled in different directions.
• Newton and Leibniz. The priority dispute over the calculus was "settled" in 1712 by a committee of the Royal Society, whose report favoured Newton; Newton, then the Society's president, wrote much of it himself and anonymously reviewed it. Today both are credited with independent invention — and the episode is a standing warning about judging one's own case.
• Kerala and Europe. The series $\frac{\pi}{4} = 1 - \frac13 + \frac15 - \cdots$ and the series for the arctangent were found by Mādhava of Saṅgamagrāma (c. 1340–1425) and his school in Kerala, centuries before Gregory and Leibniz; the name "Mādhava–Leibniz series" is now common. Similarly, the arithmetic triangle named after Pascal was known to al-Karajī and Omar Khayyam in Persia and to Jia Xian and Yang Hui in China; in China it is called Yang Hui's triangle. Stephen Stigler's "law of eponymy" (1980) — no discovery is named after its first discoverer — is, as he noted, not named after its first discoverer either.
• Credit withheld. Sophie Germain corresponded with Lagrange and Gauss under the name "Monsieur Le Blanc". Emmy Noether's lectures in Göttingen were announced under David Hilbert's name until she was allowed to habilitate in 1919. Srinivasa Ramanujan's 1913 letter to G. H. Hardy brought the work of a largely self-taught clerk in Madras to the attention it deserved. Fair attribution is also a matter of who is allowed to be seen.
• Collaboration norms. Harald Bohr recorded the "axioms" of Hardy and Littlewood's collaboration, the last being that all their papers would be joint, whatever the share of each — a humorous statement of the principle behind alphabetical order. The American Mathematical Society's statement The Culture of Research and Scholarship in Mathematics: Joint Research and Its Publication (2004) describes the alphabetical convention and its meaning.
• Errors acknowledged. Vladimir Voevodsky, in an essay of 2014, described how the proof of a key lemma in one of his own papers turned out to be wrong years after publication, and how a counterexample found by Carlos Simpson in 1998 to the main claim of a 1991 paper by Mikhail Kapranov and Voevodsky took years to be accepted. These experiences led him to devote his later work to computer-verified foundations.

• American Mathematical Society, The Culture of Research and Scholarship in Mathematics: Joint Research and Its Publication (2004), and the AMS Ethical Guidelines.
• National Academy of Sciences, On Being a Scientist: A Guide to Responsible Conduct in Research, 3rd edition (2009).
• Imre Lakatos, Proofs and Refutations: The Logic of Mathematical Discovery (1976).
• Arthur Jaffe and Frank Quinn, "'Theoretical mathematics': toward a cultural synthesis of mathematics and theoretical physics", Bulletin of the AMS 29 (1993); William P. Thurston, "On proof and progress in mathematics", Bulletin of the AMS 30 (1994).
• Nicholas J. Higham, Handbook of Writing for the Mathematical Sciences, 3rd edition (2020) — including citation practice.
• Stephen M. Stigler, "Stigler's law of eponymy", Transactions of the New York Academy of Sciences 39 (1980).
• L. J. Lander and T. R. Parkin, "Counterexample to Euler's conjecture on sums of like powers", Bulletin of the AMS 72 (1966), 1079.
• Vladimir Voevodsky, "The origins and motivations of univalent foundations", The Institute Letter (Institute for Advanced Study), Summer 2014.