Amitayush Thakur

Based on this discussion, it looks like Lean 4 may not be an ideal scratch pad for an AI trying to learn math. While some of the features in CAS...

After reading the issue: https://github.com/leanprover-community/repl/issues/25, this looks to be a similar and yet different case of the same. It seems that only linear stuff is supported in tactic mode and...

I forgot to paste the full output ```json {"cmd": "theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by sorry"}...

Also `exact hp; exact hq` won't work in REPL because it doesn't support tactical (`;`)

I just followed the example shown in the README (https://github.com/leanprover-community/repl/blob/master/README.md), I may be wrong, but it doesn't look like there is something like qed from the examples.

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 arise when you...

No use the python interface and not the native REPL to run your code. See the README https://github.com/trishullab/itp-interface (we have also tested our code on miniF2F and it works). The...

Our python code uses REPL but only for barebones Lean 4 support, we don't use pickling or tactic mode which might be prone to bugs

> Here are some minimal examples of the "Accept False Proof" bugs reported by [@RexWzh](https://github.com/RexWzh), together with errors shown in Lean. All of these proofs pass as valid in REPL's...

> [@amit9oct](https://github.com/amit9oct) `itp-interface` uses REPL's command mode to avoid false-positives, which is resource-intensive in terms of memory usage. It is necessary to fix potential bugs in tactic mode. @RexWzh Once...