Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 25, 2026Tijuana

lean Coconut

Germán Alfaro · Team German Alfaro

Submitted to The Secure Program Synthesis Hackathon. Sprint projects are early-stage work by participants, not Apart Research publications.

Read the report

Report: lean Coconut

Open in a new tab (opens in new tab)
Code (opens in new tab)
Share

We investigate whether latent chain-of-thought reasoning (Coconut; Hao et al., 2024) can improve tactic diversity and pass@k performance in Lean 4 next-tactic prediction. We train decoder-only transformers from scratch on the LeanDojo benchmark and compare standard autoregressive generation against Coconut latent-state perturbation during inference

Reviews

Judging this Sprint?

Review this project

Your public critique appears on this page without your name. Your private critique is not published; only the Apart team reads it. If you agree below, we share your review with grantmaking.ai (opens in new tab) and the Transformative AI Fund so strong projects can be funded.

Not shown on this page.

Shown on this page, without your name.

Only the Apart team reads this, and funders if you agree below.

Share my name publicly on grantmaking.ai *
Share my private critique with funders *

How much would this matter for AI safety if it worked? How innovative is it? For scores of 4-5: is this actually new to the field, or replicating recent work?

Scoring guide
  1. 1Negligible. No clear problem addressed, or no meaningful novelty.
  2. 2Limited. Addresses a real problem but with a generic or well-trodden approach. Incremental at best.
  3. 3Moderate. Clear problem with a reasonable approach; some novelty in framing or method beyond routine application of existing tools.
  4. 4Significant. Important problem with an original approach, or identifies a neglected problem area. A valuable contribution others could build on.
  5. 5Exceptional. Tackles a critical AI safety problem with a genuinely novel approach, or opens a new research direction. Clear theory of change. You'd be excited to share this with researchers in the area.

How sound are methodology, implementation, and findings?

Scoring guide
  1. 1Seriously flawed. Methodology broken, results uninterpretable, or implementation doesn't work.
  2. 2Weak. Approach has significant gaps: missing validation, flawed experimental design, or incomplete implementation.
  3. 3Competent. Technically solid given the short duration. Methodology makes sense, results are interpretable, limitations acknowledged, work builds toward clear conclusions.
  4. 4Strong. Thorough methodology with convincing validation. Results clearly support conclusions. Immediately useful for future work.
  5. 5Exceptional. Ambitious scope executed rigorously. Surprising findings, novel methods, or unusually robust validation.

How clearly are work, findings, and impact potential communicated?

Scoring guide
  1. 1Incomprehensible. Cannot determine what the project is actually claiming or doing.
  2. 2Hard to follow. Key information buried, missing, or diluted by excessive length. Significant effort to extract main points.
  3. 3Clear enough. Can understand the problem, approach, and results without undue effort. Core content clearly present: problem, method, findings, limitations.
  4. 4Well presented. Easy to follow, well-structured, appropriate level of detail. Target audience would get it quickly.
  5. 5Exceptionally clear. A pleasure to read. Complex ideas made accessible. Could serve as a model for how to present this type of work.

  1. The paper provides an interesting intersection of continuous latent reasoning and formal verification, with solid dataset auditing. However, two issues limit its impact. First, relying on exact string matching instead of a live Lean kernel is a weak evaluation choice, as it penalizes correct but syntactically different proofs. Second, the central claim about multi-stage latent steps increasing diversity does not hold on the main test set due to unresolved pipeline regressions. Incorporating live kernel verification and fixing the data and tokenizer pipeline would strengthen future versions.

  2. This paper presents a small empirical experiment in augmenting the tactic-selection capabilities of an LLM by introducing noise into the latent state before it predicts the next tactic. The hypothesis being investigated is that this latent-space perturbations will cause the agent to explore more of the tactic space (and thus have more diverse and successful attempts at proofs). The paper is clearly presented, and open about the limitations. Overall, this paper presents an interesting albeit small delta in the space of llm-based ITP automation, and an interesting result for the Hackathon.

    By building in the domain of automating proof search, this work builds upon a rich literature of historical methods of increasing diversity in tactic selection. I would be curious if the authors could build upon some of this literature, or incorporate some of the techniques previously applied in symbolic methods to LLMs. The paper also mentions that the authors did not have the time to run this on mathlib. Given that this is only a 30minute build, I would be curious to see what the results are from there. Ultimately, for the results of this paper to have more impact, I would like to see a larger comparison to existing techniques.

    Read full reviewShow less

Cite this project

@misc{alfaro2026lean,
  title = {{lean Coconut}},
  author = {Germán Alfaro},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/lean-coconut-4jwq}},
  url = {https://apartresearch.com/sprints/projects/lean-coconut-4jwq}
}

More from The Secure Program Synthesis Hackathon

All 61 entriesBrowse all projects

Build something like this at the next Sprint

AI Collusion Research Sprint · Oct 23 - 25, 2026