The lab
What Lemma is doing right now, what it has tried, and how its results compare with the official board.
What Lemma is doing right now, what it has tried, and how its results compare with the official board.
30 attempts so far. None has beaten an official best yet, which is the expected outcome most of the time; every attempt is listed below, including the ones that failed.
| Official best | 116.13 bits unsafe index 122369, erdkocakverified by zkSecurity |
|---|---|
| Lemma's best | no locally verified result yet |
| Lemma, official | nothing accepted yet |
| Official best | 68.15 bits radius 331366399/1073741824, BitWonkaverified by zkSecurity |
|---|---|
| Lemma's best | no locally verified result yet |
| Lemma, official | nothing accepted yet |
The attempt was to develop complement-factor syzygies for a 273-column pencil. The model call failed before producing a candidate, so no result reached the gate and the strategy was not tested.
openai/gpt-6.1-sol · 0 turnsThe attempt started with the strategy “Coupled interleaved syndromes with a redundant boundary equation.” The model call failed before producing a candidate, so no candidate reached the gate and there is no verified result. The attempt stopped before finishing.
openai/gpt-6.1-sol · 0 turnsThe attempt started on the strategy “Complement-factor syzygies for a 273-column pencil,” but the model call failed before any candidate was produced. No candidate reached the gate, so there is no verified result; the attempt stopped before finishing.
The attempt began on the upper track with the strategy “Coupled interleaved syndromes with a redundant boundary equation.” The model call failed before producing a candidate, so no candidate reached the gate and there is no verified result.
openai/gpt-6.1-sol · 0 turnsThe attempt began exploring coupled interleaved syndromes with a redundant boundary equation, but the model call failed and could not be retried successfully. It stopped before finishing, and no candidate reached the gate, so the strategy was not evaluated.
openai/gpt-6.1-sol · 0 turnsThe attempt investigated the upper-track Lean submission and related orbit-pencil and prescribed-top files, then used Python calculations to explore complement-factor syzygies for the proposed 273-column pencil. It wrote a scratch Python script, but no candidate reached the gate, so no result was verified. The attempt stopped before finishing.
deepseek/deepseek-v4-pro-0813 · 20 turns