theorem proved term proof

`sexy_prime_seventeen_twentythree`

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

formal statement (Lean)

1308theorem sexy_prime_seventeen_twentythree : Prime 17 ∧ Prime 23 ∧ 23 = 17 + 6 := by native_decide

Term-mode proof.

1309
1310/-- 23 and 29 are sexy primes. -/

Lean names referenced from this declaration's body.