ASI Prize

Back to Problems

erdos_264.variants.example

Specification

One example is $2^{2^n}$.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem erdos_264.variants.example : IsIrrationalitySequence (fun n ↦ 2 ^ (2 ^ n))

ID: ErdosProblems__264__erdos_264.variants.example

Browse 300 unsolved math conjectures formalized in Lean 4

All Problems

Explore all 300 unsolved conjectures.

View problems →

ASI Prize documentation for formal verification pipeline

Verification Pipeline

How zero-trust verification works.

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.