Lean version
#2
by
desaxce
- opened
Which Lean version do you recommend using?
Hi, we are using Lean 4.9. We follow DeepSeek-Prover-V1.5. You can follow their instructions to install the corresponding Lean and Mathlib.
We also filtered out the code when apply? appears together with premises such as Cardinal.toNat, Cardinal.natCast_inj, or Type*, since this is a bug reported in this blog.
We are cleaning up the code and planning to release the full test code in these days.