Open problems from research papers
2 of 10 solved in this repository.
What “solved” means here: a frozen Lean theorem in this repository is recorded against the problem. Nobody has machine-checked that the theorem says the same thing as the paper, and a problem with no record here may still have been solved by someone else.
Solved (2)
Two-parameter greedy three-sumfree membership
Proved. Lean theorem conjecture17, frozen in this repository 2026-09-06.
Problem details · Reading note · Source paper
Odd-index reduced abelian complexity of the Thue-Morse word
Proved. Lean theorem reducedAbelianComplexity_odd, frozen in this repository 2026-09-06.
Problem details · Reading note · Source paper
Not solved here (8)
Archer-Bourne cube-avoidance counting equality
Problem details · Reading note · Source paper
Classify negative base-phi prefix occurrence sequences
Problem details · Reading note · Source paper
Minimality of the base-4 golden-ratio DFAO
Problem details · Reading note · Source paper
A fourth mutually unbiased basis in dimension six
Problem details · Reading note · Source paper
Optimality of the Ordered Zeckendorf Long Game Strategy
Problem details · Reading note · Source paper
Gaussianity of random Zeckendorf game lengths via mixing
Problem details · Reading note · Source paper
Wall-Sun-Sun primes as a golden-unit lift problem
Problem details · Reading note · Source paper
Maximum order complexity along polynomial Zeckendorf subsequences
Problem details · Reading note · Source paper
How this list is made
Source revision: 55a96922.
The list is generated from problem files, reading notes, and resolution records in theorem pages at this source revision. The records are read as text, so ordinary prose can produce one; this page does not check that a record came from the repository’s own verified claim. This page does not run the repository’s checks or verify the named theorems or their Lean proofs.
The “frozen in this repository” date is the date of the first commit that added the theorem’s module to the frozen record. It is not the date the problem was solved in the world or the resolution was recorded.