Number theory
Erdős 264 - part ii
Is an example of an irrationality sequence?References
No one has attempted this yet.
Formal statement
Lean type
True ↔ Erdos264.IsIrrationalitySequence Nat.factorialWhat you must prove
import FormalConjectures.ErdosProblems.«264»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos264.erdos_264.parts.ii" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/264.lean
- Source type SHA-256
- sha256:e3245f5c060277331adfc08419f7560fb06b58348c819bd35997cf57b756b43f
- Task id
- fc-379fc029-parts-ii-b5c0483ba8-formalized-v1
- Task commitment
- sha256:3e87a2517e367f8f01e21cad8d4a4d5e19228f76d8024f3c9d51cfbc7207eb90
Something wrong with this formalization?
A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.