Catalog

Every problem here was open when it entered the pool.

Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.

Formal statement

Proof target

import FormalConjectures.GreensOpenProblems.«40»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green40.green_40.f_two_eq_one" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔ Green40.f 2 = 1

Original conjecture source: FormalConjectures/GreensOpenProblems/40.lean

Source type SHA-256: sha256:af660ea10315b3b644d0b3f001886cda5921cd09ec1966726b858f91ae264255
Task id: fc-8432eac9-green-40-f-two-eq-one-ce69be0661-formalized-v1
Task commitment: sha256:979abda716baba300e7d3d09476ff301401d93abb906d64be384c33765fe94ca

References

Green's open problem 40 - f two eq one · Conjectures.io

Every problem here was open when it entered the pool.

Green's open problem 40 - f two eq one

What has been built

Where this lives