Forward reasoning in Lean 4: sharing some work

Stream: lean4

[Siddhartha Gadgil]

I have been working for a while on attempts at forward reasoning in Lean 4. I have blogged about the results so far at https://siddhartha-gadgil.github.io/automating-mathematics/posts/forward-reasoning-in-lean4/ and the code is at https://github.com/siddhartha-gadgil/lean-loris

Any suggestions are welcome.