Q&A — Fokker Challenge

Why Lean 4?

Lean 4 is a modern proof assistant with a strong type system, fast execution, and good support for automation. It lets us encode lambda calculus reasoning formally and verify every step of the proof instead of relying on informal arguments.

Using Lean 4 also means we can combine proof search with executable code and reuse existing libraries such as cslib. This is important for the Fokker challenge because we need both rigorous formal verification and the ability to explore many candidate terms quickly.

Although we use Lean4, try hard to avoid classic logic. We hope to prove everything in constructive mathematics.

Why LocallyNameless?

When representing variables in lambda calculus or proof assistants, the three most common approaches are named variables, de Bruijn index, and locally nameless.

We chose locally nameless because cslib offers the most comprehensive support, and we have contributed a lot to cslib as well.

How does this compare to related collaborative projects?

teorth/equational_theories

Modern AI (LLMs like GPT, Claude, etc.) was NOT heavily used for the core work.

Busy Beaver (BB Challenger)

Is another search-driven formal challenge. It is similar because it targets the smallest programs with extreme behavior, but the Fokker challenge has fewer unsolved cases in its current search space and is more immediately approachable with AI-guided reasoning.

Similarities and Differences

Similar: all these projects are about combining formal methods with search, exploring the boundary of what can be proven automatically, and managing a tight space of candidate structures. We will all make extensive use of AI.

Less unsolved cases: the current Fokker challenge scope is bounded by small Fokker size and a finite set of candidate terms. That makes it more tractable than broad open problems such as general equational theories or the full busy beaver landscape.

More difficult work: the hard part here is not just brute force, but recognizing patterns in lambda terms and developing new deciders. This means the project benefits from AI that can synthesize structural insights, not only compute exhaustively.

More previous papers: We are currently still assimilating the achievements of our predecessors and formalizing them.

Decidability In bbchallenge, based on current mathematical knowledge, some TMs are impossible to determine halting. But in Fokker challenge, we believe every term is decidable.

Will we write a paper?

If we prove some non-trival theorems, we will write a paper.

Plan after Fokker challenge finish

We plan to verify the smallest single-point basis, measured in bits using Binary Lambda Calculus