Jason Rute

I think your point @jesse-michael-han is that as long as good data is used for training, then these proof checks error are really not going to come up and one...

While I think it doesn't make sense to filter the training data in lean-gym, I suppose one could filter the proofs a bit more in `lean_proof_recording` using a similar idea....

Also, let me better explain my worry. Suppose my AI comes up with the following trajectory for this (obviously contrived) example ``` example : ∀ (a b c > 0),...

One more comment. Obviously, upstream actions effect downstream rewards and this is a common problem in RL, the credit assignment problem. Nonetheless, there is an assumption here, at least within...

I was thinking as doc strings in the `commands.py` file. That way if you are in an IDE which supports doc strings, it can tell you want to expect from...

Yes, I've have been meaning to do something about this. The biggest difference between that paper and mine is that in their tests, they let the solver run for 1...

I agree we should check Qt code before merging. I just haven't got around to running it yet.

Specifically, the problems start in Lean 3.15.0. Here is an error when doing an info command: ``` Traceback (most recent call last): File "/tmp/mathlib/scripts/find_and_replace.py", line 152, in trio.run(main, path, old,...

I'm not sure what you mean by "lean core development" and "there". Are you talking about the [lean repo](https://github.com/leanprover-community/lean)? A thread/stream on Zulip? Somewhere else?

@EdAyers I think we want to support widgets (They are a cool feature!), but maybe in the future, we can get a heads-up here (in the form of an issue...