Lean Intuition asks whether expensive proof search can train a cheaper heuristic that improves theorem completion under a fixed total computation budget.
Approach
A bounded tactic search records the theorem, proposed actions, accepted and rejected steps, resulting goals, and consumed budget. A ranker learns from those traces and changes which search paths are explored first.
The implementation includes a linear ranker and an optional encoder-based ranker. Lean checks candidate steps, while a separate final compilation checks the completed source. Keeping every simultaneous goal together matters: solving one branch does not finish a theorem with other goals remaining.
This is an initial research implementation, not an established trained prover. Demonstration traces from mock environments cannot count as verified theorems or evidence of generalization.
The main comparison must include the cost of the learned heuristic as well as the search it saves. Faster selection is only useful if it leads to more formally verified completions within the same overall budget.