Skip to content

Paperproof v2.4.0

Choose a tag to compare

@lakesare lakesare released this 22 Jul 05:59
· 75 commits to main since this release
c5a3e62

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.