Documentation Verification Report

Goldbach

📁 Source: PrimeNumberTheoremAnd/Goldbach.lean

Statistics

Metric	Count
Definitions `even_conjecture`, `odd_conjecture`	2
Theorems `e_silva_herzog_piranian_goldbach`, `e_silva_herzog_piranian_goldbach_ext`, `even_conjecture_mono`, `even_goldbach_test`, `even_to_odd_goldbach`, `even_to_odd_goldbach_triv`, `helfgott_odd_goldbach_finite`, `kadiri_lumley_odd_goldbach_finite`, `odd_conjecture_mono`, `odd_goldbach_test`, `ramare_saouter_odd_goldbach`, `richstein_goldbach`	12
Total	14
⚠️ With sorry `e_silva_herzog_piranian_goldbach`, `e_silva_herzog_piranian_goldbach_ext`, `even_to_odd_goldbach_triv`, `kadiri_lumley_odd_goldbach_finite`, `richstein_goldbach`	5

Goldbach

Definitions

Name	Category	Theorems
`even_conjecture` 📖	MathDef	4 math math: `even_goldbach_test`, `e_silva_herzog_piranian_goldbach`, `richstein_goldbach`, `e_silva_herzog_piranian_goldbach_ext`
`odd_conjecture` 📖	MathDef	5 math math: `helfgott_odd_goldbach_finite`, `kadiri_lumley_odd_goldbach_finite`, `even_to_odd_goldbach_triv`, `ramare_saouter_odd_goldbach`, `odd_goldbach_test`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`e_silva_herzog_piranian_goldbach` 📖 ⚠️	mathematical	—	`even_conjecture`	—	—
`e_silva_herzog_piranian_goldbach_ext` 📖 ⚠️	mathematical	—	`even_conjecture`	—	—
`even_conjecture_mono` 📖	—	`even_conjecture`	—	—	—
`even_goldbach_test` 📖	mathematical	—	`even_conjecture`	—	—
`even_to_odd_goldbach` 📖	—	`HasPrimeInInterval` `even_conjecture` `odd_conjecture`	—	—	`odd_conjecture_mono` `even_to_odd_goldbach_triv` `odd_goldbach_test`
`even_to_odd_goldbach_triv` 📖 ⚠️	mathematical	`even_conjecture`	`odd_conjecture`	—	—
`helfgott_odd_goldbach_finite` 📖	mathematical	—	`odd_conjecture`	—	`even_to_odd_goldbach` `RamareSaouter2003.has_prime_in_interval` `e_silva_herzog_piranian_goldbach` `odd_conjecture_mono` `even_to_odd_goldbach_triv`
`kadiri_lumley_odd_goldbach_finite` 📖 ⚠️	mathematical	—	`odd_conjecture`	—	—
`odd_conjecture_mono` 📖	—	`odd_conjecture`	—	—	—
`odd_goldbach_test` 📖	mathematical	—	`odd_conjecture`	—	`even_to_odd_goldbach_triv` `even_goldbach_test`
`ramare_saouter_odd_goldbach` 📖	mathematical	—	`odd_conjecture`	—	`even_to_odd_goldbach` `RamareSaouter2003.has_prime_in_interval` `richstein_goldbach` `odd_conjecture_mono` `even_to_odd_goldbach_triv`
`richstein_goldbach` 📖 ⚠️	mathematical	—	`even_conjecture`	—	—

---

← Back to Index