Lean 4 LLMs
TODO
-
Survey existing Lean 4 LLMs and their capabilities
- Types
- Theorem Proving
- single step models
- whole proof
- premise selection
- auto- formalization / auto-informalization
- Theorem Proving
- Types
-
Dissection of key models
- focus on how to use for inference rather than how they were trained
- prompt format, base model, size
- engineering bits:
- tokens per sec a100/h100, context window
-
code to recreate published benchmark results
-
small experiments testing robustness (slight variations in prompts, context size, etc.)