Edit model card

miniCTX: Neural Theorem Proving with (Long-)Contexts

State-tactic model from miniCTX: Neural Theorem Proving with (Long-)Contexts.

It is specifically finetuned for Lean 4 tactic prediction given proof states.

Performance

Please see our paper.

Example input

/- You are proving a theorem in Lean 4.
You are given the following information:
- The current proof state, inside [STATE]...[/STATE]

Your task is to generate the next tactic in the proof.
Put the next tactic inside [TAC]...[/TAC]
-/
[STATE]
m n : â„•
h : Nat.Coprime m n
⊢ Nat.gcd m n = 1
[/STATE]
[TAC]

Example output

rw [Nat.Coprime] at h
[/TAC]

Citation

Please cite:

@misc{hu2024minictx,
  title={miniCTX: Neural Theorem Proving with (Long-)Contexts}, 
  author={Jiewen Hu and Thomas Zhu and Sean Welleck},
  year={2024},
  eprint={2408.03350},
  archivePrefix={arXiv},
  primaryClass={cs.AI},
  url={https://arxiv.org/abs/2408.03350}, 
}
Downloads last month
35
Inference Examples
This model does not have enough activity to be deployed to Inference API (serverless) yet. Increase its social visibility and check back later, or deploy to Inference Endpoints (dedicated) instead.

Collection including l3lab/ntp-mathlib-st-deepseek-coder-1.3b