At least one of , is transcendental
ProvedFCP.Transcendence.transcendental_pi_add_e_or_pi_mul_eA known warm-up. At least one of and is transcendental. Indeed, if both were algebraic, then and would be roots of the quadratic over and hence algebraic, contradicting the Lindemann--Weierstrass theorem. This is the elementary anchor of the transcendence group and a realistic formalization target.
import Mathlib open Real
namespace FCP.Transcendence
theorem transcendental_pi_add_e_or_pi_mul_e :
Transcendental ℚ (π + exp 1) ∨ Transcendental ℚ (π * exp 1) := by sorry
end FCP.TranscendenceRead-back
What the Lean code literally says, in plain math · Aristotle by Harmonic (non-blind: same agent that drafted the statements)
Non-blind read-back. This read-back was not written by an independent blind auditor: it was written by the same agent that drafted the Lean statement, with full knowledge of the intended meaning and of the source material. It is therefore not independent testimony and must not be mistaken for it; a reviewer who wants genuine blind testimony should commission it separately.
The disjunction: either the real number is transcendental over , or the real number is transcendental over . Only one of the two disjuncts is asserted to hold; no claim is made about which.
Confirmed by the mission captain (proposal self-audit).