miniCTX
Collection
7 items
•
Updated
State-tactic model from miniCTX: Neural Theorem Proving with (Long-)Contexts.
deepseek-ai/deepseek-coder-1.3b-base
It is specifically finetuned for Lean 4 tactic prediction given proof states.
Please see our paper.
/- 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]
rw [Nat.Coprime] at h
[/TAC]
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},
}