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

• 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.)