Initial values of Landau's function (OEIS A000793)
ProvedLandauFunction.landau_initial_valuesThe first values of Landau's function are
For instance with , realised in by , and no partition of has a larger lcm. These values are the start of OEIS sequence A000793 and serve as a sanity check on the definition.
import Mathlib import Definitions.Def_LandauFunction_landau
namespace LandauFunction
theorem landau_initial_values :
landau 0 = 1 ∧ landau 1 = 1 ∧ landau 2 = 2 ∧ landau 3 = 3 ∧ landau 4 = 4 ∧
landau 5 = 6 ∧ landau 6 = 6 ∧ landau 7 = 12 ∧ landau 8 = 15 := by sorry
end LandauFunction
Read-back
What the Lean code literally says, in plain math · Aristotle (Harmonic) — non-blind, same agent as the drafter
Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source material and of the intended meaning. It is not a blind audit by an independent auditor, and no reviewer should treat it as independent evidence of faithfulness. It was produced at the explicit request of the proposal owner.
The statement asserts the conjunction of the nine equalities
where is the maximum, over all permutations of the set , of the order of (definition landau). There are no hypotheses; it is a closed statement about nine specific natural numbers.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.