leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: Save Context and Goal at Each Step of a Proof in Lean


White Chen (Sep 02 2024 at 14:37):

In Lean, I want to save the context and goal before and after each step (line?) of a proof. I know that LeanDojo can accomplish this, but it seems not convenient enough. Is there a simpler method to achieve this?

Jason Rute (Sep 02 2024 at 18:38):

I’ve used https://github.com/semorrison/lean-training-data for this.


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll