Pisano is even from three to fifty

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.

Proposition

(List.range 48).all (fun i => pisano (i + 3) != 0 && pisano (i + 3) % 2 == 0) = true

Proof

By decide +kernel in registry.lean. Checked by the Lean kernel: it depends on no axiom.

Sources and identifiers

• Lean source · src/pair/lean/proofs/registry.lean
• Typeset paper · src/research/lean-theorems.tex
• Repository deposit · doi:10.5281/zenodo.21787144
• Author · ORCID 0009-0000-7312-9778

Proved in the same file

• Sothic cycle meshes
• Sothic cycle days
• Vdw nine forces
• Vdw eight escapes
• Condorcet profiles are 216
• Condorcet six cycle
• Graeco latin none of order two
• Graeco latin order three
• Graeco latin order four
• Graeco latin order five
• Kummer instances
• Tau six is product
• K5 k33 break planar bounds
• Catalan heptagon
• Exactly three regular tilings
• Steiner two three seven
• Heawood moore bound
• Exactly five platonic solids
• Pisano ten is sixty
• Pisano nine is twenty four
• Pisano reads sixty at ten
• Cassini step negates
• Cassini for every n
• Catalan parity is mersenne
• Fibonacci partial sum for every n
• Lucas is the sum of the fibonacci neighbours
• Lucas fibonacci identity for every n
• Triangular closed form for every n
• Odd sum is a square for every n
• Pyramidal closed form for every n
• Nicomachus for every n
• Gray code is a one bit cycle to twelve
• Hockey stick to twenty
• Vandermonde convolution to twelve
• Amicable 220 284 is the smallest
• The three digit armstrong numbers are four
• Taxicab two is 1729
• Euler polynomial is prime to 39 then 41 squared
• Fermat five is composite
• Frobenius six nine twenty misses 43
• Frobenius six nine twenty reaches every n from 44
• Schur two is four
• Z doubling orbit lies in the units on odd moduli
• Z order of two divides the unit count on odd moduli
• Z two is no unit on even moduli
• Z reflection is an involution and partitions
• Z fibonacci period returns and is even beyond two
• Z nine orbit is the vortex sequence
• Circle of fifths does not close

All machine-checked theorems