pith. machine review for the scientific record. sign in
theorem proved term proof

six_almost_prime_sevenhundredtwentynine

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

2743theorem six_almost_prime_sevenhundredtwentynine : isSixAlmostPrime 729 = true := by native_decide

proof body

Term-mode proof.

2744
2745/-! ### Weak primes (p < (p_prev + p_next)/2) -/
2746
2747-- Note: 3 < (2 + 5)/2 = 3.5, but in ℕ, (2+5)/2 = 3, so 3 < 3 is false. 3 is balanced.
2748
2749/-- 7 is a weak prime: 7 < (5 + 11)/2 = 8. -/

depends on (6)

Lean names referenced from this declaration's body.