Overview

In this release Paperproof finally gets its own domain, 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.

  

• Renderer
  Go to 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

  @celainica contributed terminal.lean (link), a script that lets you use Paperproof from within a terminal. This is useful for data processing in AI applications.

  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
  

  you can run lake exe terminal myFile.lean simple_proof myOutput.json, and get the following output:

  [{
    "theorems": [],
    "tacticString": "apply And.intro",
    "tacticDependsOn": ["_uniq.11", "_uniq.12"],
    "spawnedGoals": [],
    "position": {"stop": {"line": 0, "character": 0}, "start": {"line": 0, "character": 0}},
    "goalsAfter": [
      {
        "username": "left", "type": "p", "id": "_uniq.22",
        "hyps": [
          {"value": null, "username": "p", "type": "Prop", "isProof": "universe", "id": "_uniq.11"},
          {"value": null, "username": "q", "type": "Prop", "isProof": "universe", "id": "_uniq.12"},
          {"value": null, "username": "hp", "type": "p", "isProof": "proof", "id": "_uniq.13"},
          {"value": null, "username": "hq", "type": "q", "isProof": "proof", "id": "_uniq.14"}
        ]
      },
      {
        "username": "right", "type": "q", "id": "_uniq.23",
        "hyps": [
          {"value": null, "username": "p", "type": "Prop", "isProof": "universe", "id": "_uniq.11"},
          {"value": null, "username": "q", "type": "Prop", "isProof": "universe", "id": "_uniq.12"},
          {"value": null, "username": "hp", "type": "p", "isProof": "proof", "id": "_uniq.13"},
          {"value": null, "username": "hq", "type": "q", "isProof": "proof", "id": "_uniq.14"}
        ]
      }
    ],
    "goalBefore": {
      "username": "[anonymous]", "type": "p ∧ q", "id": "_uniq.15",
      "hyps": [
        {"value": null, "username": "p", "type": "Prop", "isProof": "universe", "id": "_uniq.11"},
        {"value": null, "username": "q", "type": "Prop", "isProof": "universe", "id": "_uniq.12"},
        {"value": null, "username": "hp", "type": "p", "isProof": "proof", "id": "_uniq.13"},
        {"value": null, "username": "hq", "type": "q", "isProof": "proof", "id": "_uniq.14"}
      ]
    }
  }, {
    "theorems": [],
    "tacticString": "exact hp",
    "tacticDependsOn": ["_uniq.13"],
    "spawnedGoals": [],
    "position": {"stop": {"line": 0, "character": 0}, "start": {"line": 0, "character": 0}},
    "goalsAfter": [],
    "goalBefore": {
      "username": "left", "type": "p", "id": "_uniq.22",
      "hyps": [
        {"value": null, "username": "p", "type": "Prop", "isProof": "universe", "id": "_uniq.11"},
        {"value": null, "username": "q", "type": "Prop", "isProof": "universe", "id": "_uniq.12"},
        {"value": null, "username": "hp", "type": "p", "isProof": "proof", "id": "_uniq.13"},
        {"value": null, "username": "hq", "type": "q", "isProof": "proof", "id": "_uniq.14"}
      ]
    }
  }, {
    "theorems": [],
    "tacticString": "exact hq",
    "tacticDependsOn": ["_uniq.14"],
    "spawnedGoals": [],
    "position": {"stop": {"line": 0, "character": 0}, "start": {"line": 0, "character": 0}},
    "goalsAfter": [],
    "goalBefore": {
      "username": "right", "type": "q", "id": "_uniq.23",
      "hyps": [
        {"value": null, "username": "p", "type": "Prop", "isProof": "universe", "id": "_uniq.11"},
        {"value": null, "username": "q", "type": "Prop", "isProof": "universe", "id": "_uniq.12"},
        {"value": null, "username": "hp", "type": "p", "isProof": "proof", "id": "_uniq.13"},
        {"value": null, "username": "hq", "type": "q", "isProof": "proof", "id": "_uniq.14"}
      ]
    }
  }]
  

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:

  

  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]`
    ...
    h2: x ∈ t ∧ x ∈ s
    ________________________________________________________________
    ...
    h2: x ∈ s ∧ x ∈ t
  
  ******************************************************************
  
  TACTIC 10: `exact h2`
    CLOSED: x ∈ s ∩ t
  
  ******************************************************************
  
  

  This makes use of Paperproof's diffing algorithm, the output only contains the parts that were indeed changed by the tactic.

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.

This UI is very similar to the default InfoView, with one important distinction - instead of showing the diff (by highlighting the substrings of the hypothesis/goal that changes), we simply display the "before" and the "after" types, one below the other.

The usual paperproof niceties stay around too - hypotheses are color-coded (proof vs data), hypotheses that were used by the tactic are highlighted, and you can see the used theorem's signature side-by-side to pattern match it to the effect the tactic took.

Essentially, this interface is meant to shorten the repetitive action of "click on the line before the tactic; click on the line after the tactic; hover over the theorem definition" - a single click on the tactic line should suffice to understand what exactly this tactic line is doing.

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.

  

  All theorem names present in a tactic are underlined. When you click on the theorem name, you can see that theorem's signature:

  

• 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".

  

• Logs for LLMs

  If you'd like your llm to quickly understand the structure of some proof, you can CMD+SHIFT+P: Open Webview Developer Tools, click within some proof, and copypaste the console.logged valued called "copypaste". Per each tactic, it will produce the following output:

  tactics: [ 
   ...,
   {
     text: "intro h1",
     hypothesisChanges: [{ from: null, to: ["x ∈ s ∩ t"] }],
     goalChanges: [{ from: "x ∈ s ∩ t → x ∈ t ∩ s", to: "x ∈ t ∩ s" }],
     closedSomeGoal: null
   },
   ...
  ]
  

  This makes use of Paperproof's diffing algorithm, the output only contains the parts that were indeed changed by the tactic.

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.

  

• Bolden tactics
  Based on user's cursor position in VSCode editor.

  

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.

  BEFORE	NOW

  This is generally good UX for proofs of any size, but it's particularly important in real formalization projects, makes large proofs a lot more readable.

• preliminary implementation of hide/show buttons for have boxes

  On this image, you can see ⛶ and ▬ buttons.
  ⛶ expands the (collapsed) box, ▬ collapses the (expanded) box

  

  This UI needs to be worked on (for example, nothing should move when we click these buttons!), but it's sure better than the collapsing logic we had before.

• hide hypotheses with ✝ in the name
  When we do rcases h with ⟨h1, _⟩, Lean will give us h1 : J ∈ 𝓙 (t.𝔖₀ u₁ u₂) and right✝ : J ∈ Iic (𝓘 u₁).
  From now on, we assume the user used _ because they are not interested in seeing right✝ : J ∈ Iic (𝓘 u₁) , and so we hide ✝-ed hypotheses.

Added

• Settings are saved now
  Every time you toggle settings, they get saved in your vscode User Settings.

  

• 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.

  

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 #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

BEFORE	AFTER

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.

  Hide goal names: off	Hide goal names: on

• Added an option "Always green hypotheses"
  Again - this is to ease beginner's understanding of Paperproof proofs. Additional colors do ease the reading of a proof, but might be confusing initially. From now on, we let people turn on this functionality when they are ready for it.

  Always green hypotheses: off	Always green hypotheses: on

• Made it possible to render Paperproof in github codespaces

  Just go to github.com/codespaces/new/Paper-Proof/paperproof and wait for a few minutes for your codespace to load.
  That usually takes 2-4 minutes.
  If you have a Lean repo, and you would like to enable codespaces in it, all it takes is these two files: .devcontainer.
  If you would like to enable Paperproof in your codespaces, just add "extensions": ["leanprover.lean4@0.0.176", "paperproof.paperproof"] (note that we fix the leanprover.lean4 extension version - this makes sure leanprover.lean4 extension updates don't break your codespace).

  Here is what it will look like:

  

Changed

• Changed the way initial hypotheses are displayed
  Previously we had a fake init tactic. Now, we changed it to "HYPOTHESES" header.

  BEFORE	NOW

• Changed the font and variable colors
  Here we both move towards and away from Lean's default InfoView.
  We changed our font to match the one Lean's InfoView uses - it renders mathematics symbols much more clearly than our previous font.
  On the other hand, we changed the variable color from the orange color (used in Lean's InfoView) to dark pink, which is easier to read on our green node backgrounds.

  BEFORE	NOW

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
  

In general - Paperproof was fully rewritten (we went from Tldraw to vanilla React). Interaction with Paperprooof feels different now, it's just a normal webpage that you can scroll around.