language

python，with edge size 363475 and node size 29611。 exception code line is: 

Now I change the codes as below,it's running with out exception,but still slowly. 

> I found another example where the REPL accepts an incorrect proof: > > [amc12a_2002_p12](https://github.com/wzj423/lean-dojo-mew/blob/d08b8ba9bad48a7a6497bad6fde21bace85128e2/MiniF2F/Validation.lean#L1016C1-L1017C97) from minif2f. > > ``` > import Mathlib > theorem amc12a_2002_p12 (f : ℝ →...

> You can use our tool: https://github.com/trishullab/itp-interface > > It is based on REPL but doesn't accept wrong proofs. It also allows parallel proof execution, handling memory issues which might...