Paper-Proof/paperproof

📦 Overview

• In this release, Paperproof makes it possible to see Lean code as LaTeX!
• [Screencast from 2026-04-05 03-01-04.webm](https://github.com/user-attachments/assets/20160bdb-d9ea-49e6-883f-9c4d7b12ce1d)

✨ Added

• Display any Lean proof in LaTeX
• <table>
• <tbody>
• <tr>
• <th>Lean</th>
• <th>LaTeX</th>
• </tr>
• <tr></tr>
• + 13 more

🐛 Fixed

• Lean versioning fixed
• From now on, your Lean version won't be getting automatically increased upon Paperproof import unless it's absolutely necessary (we didn't know Lean does that, sorry!).
• Fixed "PANIC at List.head!" error
• Paperproof was raising this error from time to time with no stack trace. That's fixed now.

📦 Overview

• In this release Paperproof finally gets its own domain, [paperproof.xyz](https://paperproof.xyz/), with two accompanying features - snapshots and natural-language proof renderer.

✨ Added

• Snapshots
• You can now create a snapshot of any proof, and get a shareable link.
• For example, here is what we get by snapshotting the proof below: [paperproof.xyz/b7f2e8b00caf0e63](https://paperproof.xyz/b7f2e8b00caf0e63).
• <img width="800" alt="image" src="https://github.com/user-attachments/assets/2e0fe4e7-285f-4cb3-8c89-24ebeba17a39" />
• Renderer
• Go to [paperproof.xyz](https://paperproof.xyz), paste any json, and get a paperproof tree rendered.
• This is a bit raw in its current state, but the idea is that eventually we should be able to render any natural-language proof in paperproof notation.

✨ Added

• Use Paperproof's parser from the terminal
• For example, if you have the following theorem in `myFile.lean` file:
• ```
• theorem simple_proof (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
• apply And.intro
• exact hp
• exact hq
• ```
• + 71 more

📦 Updated

• Made Paperproof support Lean v4.24.0.

✨ Added

• Logs for LLMs
• If you'd like your llm to quickly understand the structure of some proof, you can right-click on the proof, and select "Copy for LLM" option:
• <img width="400" src="https://github.com/user-attachments/assets/46a2347e-1aa7-4fbb-9474-58348cc6e7ec" />
• This will copy the proof structure to your clipboard, which will look something like this:
• ```
• TACTIC 1,2,3,4,5,6,7,8...
• TACTIC 9: `rw [and_comm]`
• ...
• + 10 more

🐛 Fixed

• Zoom-in/Zoom-out context menu options now also appear in the Single-Tactic Mode
• Zoom-in/Zoom-out shortcuts now also work on Linux
• Previously the `ALT+` and `ALT-` shortcuts weren't working on Linux machines, now this is more robust.

📦 Overview

• This release introduces an experimental UI for Lean 4: a Single-Tactic Mode.
• Single-Tactic Mode is primarily useful during the process formalization. This mode works well on proofs of any size, and shows all information the default InfoView might show.

✨ Added

• New UI mode: "Single-Tactic Mode"
• Notice how a cursor set at `rw [Set.mem_inter_iff, and_comm] at h1` only displays the effect the `rw` created, ignoring the rest of the proof.
• <img width="800px" src="https://github.com/user-attachments/assets/2b663140-1a09-4943-9511-03e9f0ea0536"/>
• All theorem names present in a tactic are underlined. When you click on the theorem name, you can see that theorem's signature:
• <img width="400px" src="https://github.com/user-attachments/assets/03c4bc5e-2817-481d-88ed-bb5e7549b62a"/>
• New context menu action: "Hide hypothesis"
• In both modes, you can now hide a bulky hypothesis node by right-clicking on it and selecting "Hide hypothesis".
• <img width="400px" src="https://github.com/user-attachments/assets/889e5c44-bf88-4a76-bf63-93948b07b1a4"/>
• + 14 more

📦 Overview

• Improvements that make scopes ("what hypotheses are in scope", "what tactic is the cursor currently on") easy to track.

✨ Added

• Highlight available hypotheses and goals
• Based on what hypotheses and goals are currently in scope.
• <img width="200px" src="https://github.com/user-attachments/assets/8f43886c-e942-4aa7-a77c-bf597c0443cd">
• Bolden tactics
• Based on user's cursor position in VSCode editor.
• <img width="200px" src="https://github.com/user-attachments/assets/9a16ecec-777c-4ecf-87af-368b868d8e07">

📋 Changed

• Remove isReadonlyMode setting
• Changes described above make scoping nonintrusive, so we don't need to have an additional setting that controls whether we want UI indicating scoping on or off; now it's always on.

📦 Overview

• Changes that make working on real formalization projects with Paperproof easier.
• only show spawned `by` boxes when we are working on them
• Suppose we have a tactic `apply (le_mul_inv_iff₀ (by positivity)).mpr`, as seen below.
• This tactic has a "spawned goal" `0 < 2 ^ (100 * a)`, a goal that we're proving in the `by positivity` block.
• Previously, we were showing these spawned goals as normal subgoals (left picture).
• Now we're hiding them (right picture), and only showing them when our cursor is directly in that `by positivity` block.
• <table>
• <tbody>
• + 24 more

✨ Added

• Settings are saved now
• Every time you toggle settings, they get saved in your vscode User Settings.
• <img width="200px" src="https://github.com/user-attachments/assets/ab4fee81-db1c-4fc0-a5e8-7014f3a4e907"/>
• Added a spinning loading icon
• When Paperproof is thinking, you will now see a pink spinning coin.
• 

📦 Overview

• Changes that make working on real formalization projects with Paperproof easier.

✨ Added

• Handle `#exit` gracefully
• If your cursor is placed after the `#exit` command, Paperproof will tell you about it.
• <img width="320" alt="image" src="https://github.com/user-attachments/assets/ede94ab1-8b64-454f-84fa-83bf7d8e644b">

📋 Changed

• Removed floating hypotheses
• They were not working very well for large proofs.
• Made Paperproof NOT affect performance of the default InfoView
• Made it so that when the Paperproof panel is closed, rpc requests don't get sent (see https://github.com/Paper-Proof/paperproof/issues/51).
• Easier text selection in goals and hypotheses
• Previously, when you tried selecting some text from the goal or a hypothesis node, Paperproof would zoom in on the box you clicked on. Now this zoom won't happen during the "select" motion.

📦 Overview

• <table>
• <tbody>
• <tr>
• <th>BEFORE</th>
• <th>AFTER</th>
• </tr>
• <tr></tr>
• <tr>
• + 9 more

✨ Added

• Added an option "Hide goal names"
• Goal names (see, for example, a grey box with `"right.left"` written on them) are immensely helpful during some types of proofs, for example when we do induction proofs about functions.
• In some proofs, however, goal names just clutter the interface, and it should be possible to hide them.
• From now on, we hide the goal names by default, in the spirit of making the initial interface perfectly intelligible to the Paperproof novice.
• <table>
• <tbody>
• <tr>
• <th>Hide goal names: off</th>
• + 37 more

📋 Changed

• Changed the way initial hypotheses are displayed
• Previously we had a fake `init` tactic. Now, we changed it to "HYPOTHESES" header.
• <table>
• <tbody>
• <tr>
• <th>BEFORE</th>
• <th>NOW</th>
• </tr>
• + 41 more

📋 Changes

• Paperproof works offline now, too
• Tactic combinators get properly displayed
• Added various modes that change how the proof is displayed: compact mode, compact tactics mode, readonly mode
• Upon right-clicking on a particular box, you can collapse it now
• Hypotheses have grey, yellow, and green colors - grey ones is sorts which we do not show; yellow ones is data; green ones is proofs