Probe of the publication statement layout

Proved

OddPerfectNumber.Kernel.dris_five_probe_layout

by WillR · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theory

A layout probe used to diagnose a publication validator fault. It states a trivial implication about natural numbers and is not intended to be proved.

Formal statement

namespace OddPerfectNumber.Kernel

theorem dris_five_probe_layout (a b : Nat) (h : a = b) : b = a := by
  sorry

end OddPerfectNumber.Kernel

Source

Diagnostic probe; not a mathematical claim.

View graph