What the work involves

Day to day you move between three modes. The first is straight formalization: take a written statement and proof — a competition problem, a textbook theorem, sometimes a research-level lemma — and produce Lean 4 that compiles against current mathlib, using the idiomatic definitions rather than a hand-rolled parallel universe of your own. The second is statement-fidelity review: reading a formal statement beside its informal source and deciding whether it is faithful, vacuous, over-strengthened, or quietly assuming away the hard case. The third is adversarial review of model output — finding the `sorry` that was hidden behind an unfolded definition, the hypothesis that makes the goal trivially true, the `Nat` subtraction that changed the claim — and writing feedback precise enough that a researcher can act on it.

You will also be pulled into rubric work: helping define what "good proof" and "faithful statement" mean operationally, so that judgments stay consistent across a team of Lean engineers. Expect disagreement cases to come back to you, and expect to defend a call in writing.

What the screen looks for

  • Evidence you have actually shipped Lean. Mathlib PRs, a formalization repo, a tactic or library, autoformalization work. Named artifacts beat described enthusiasm.
  • Mathlib navigation under pressure. Whether you know how to find the right lemma — `exact?`, `loogle`, naming conventions, the relevant algebraic hierarchy — rather than reproving things from scratch.
  • Proof-based mathematical depth, through a degree or research record, in algebra, analysis, number theory, combinatorics or logic.
  • Fidelity instinct. The recurring probe is a statement that typechecks and is wrong; you should be able to say precisely why.

Logistics

Remote, W-2 through Cincinnatus LLC (or the appropriate international entity), with placement into a leading AI lab's extended workforce. Minimum 20 hours per week with weekday overlap for collaboration and review cycles, scalable to 40. Observed pay band is $90–110/hr; bands are as reported, not guaranteed. Work is reviewed and cross-checked, so consistency across many small judgments matters as much as the occasional hard formalization.