A sum of consecutive odd primes is extra composite

Description:

We say two prime numbers are consecutive if there are no prime numbers between them.

In this kata, you prove the following fact about consecutive primes : if p and q are consecutive primes strictly greater than 2, then p + q can be written as a product of three numbers, each strictly greater than 1.

This problem comes from "Mathematical Recreations And Essays" by Rousse-Ball & Coxeter. (The author of this kata learned about it from this reddit post: https://www.reddit.com/r/mathriddles/comments/7f9l7a/let_pq_be_consecutive_primes_greater_than_2_show/?utm_source=share&utm_medium=web2x)

Preloaded

The full source code of Preloaded.lean is displayed below for your reference:

import data.nat.prime

def SUBMISSION := ∀ p q,
  nat.prime p →
  nat.prime q →
  p < q →
  p ≠ 2 →
  q ≠ 2 →
  (∀ k, p < k → k < q → ¬ nat.prime k) →
  ∃ a b c, p + q = a * b * c ∧ a > 1 ∧ b > 1 ∧ c > 1
notation `SUBMISSION` := SUBMISSION

Number Theory

Puzzles

Similar Kata:

More By Author:

Check out these other kata created by khanh93

Stats:

Created	May 5, 2020
Published	May 5, 2020
Warriors Trained	82
Total Skips	13
Total Code Submissions	31
Total Times Completed	19
Lean Completions	19
Total Stars	4

% of votes with a positive feedback rating	100% of 7
Total "Very Satisfied" Votes	7
Total "Somewhat Satisfied" Votes	0
Total "Not Satisfied" Votes	0
Total Rank Assessments	4
Average Assessed Rank	6 kyu
Highest Assessed Rank	6 kyu
Lowest Assessed Rank	6 kyu

Kata