Search results

goal_tactic does not work for certain tactics, as compared to Lean4 or load_sorry

bugSomething isn't workingSomething isn't working

pending-integrationUpstream feature has implemented. Pending API ImplementationUpstream feature has implemented. Pending API Implementation

Status: Open.

#82 In stanford-centaur/PyPantograph;

· attilajam opened on Mar 11, 2025

Running Pantograph on newer version of Lean

pending-integrationUpstream feature has implemented. Pending API ImplementationUpstream feature has implemented. Pending API Implementation

Status: Open.

#80 In stanford-centaur/PyPantograph;

· austinletson opened on Feb 23, 2025

load_sorry fails to recognize open statements

Status: Open.

#79 In stanford-centaur/PyPantograph;

· AG161 opened on Feb 21, 2025

Doc backlog

documentationImprovements or additions to documentationImprovements or additions to documentation

Status: Open.

#76 In stanford-centaur/PyPantograph;

· lenianiva opened on Feb 9, 2025

Feature Request: Split Pantograph and PyPantograph

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#75 In stanford-centaur/PyPantograph;

· RexWzh opened on Feb 5, 2025

Unexpected compilation errors and errors in ProofNet Lean4 dataset

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#74 In stanford-centaur/PyPantograph;

· brando90 opened on Jan 31, 2025

Reproducible instructions for installing and building Mathlib4

Status: Open.

#73 In stanford-centaur/PyPantograph;

· brando90 opened on Jan 30, 2025

How to use mathlib without creating a lean project?

Status: Open.

#72 In stanford-centaur/PyPantograph;

· brando90 opened on Jan 29, 2025

How to implement "compilation check" for AutoFormalization (only if the Lean 4 is syntactically valid, has any bug)

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#71 In stanford-centaur/PyPantograph;

· brando90 opened on Jan 28, 2025

Pantograph doesn't work when a debugger is one eg vscode debugger

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#70 In stanford-centaur/PyPantograph;

· brando90 opened on Jan 28, 2025

Change tactic_feedback in agent to SearchState

enhancementNew feature or requestNew feature or request

feature/searchSearch and agentsSearch and agents

Status: Open.

#40 In stanford-centaur/PyPantograph;

· lenianiva opened on Oct 23, 2024

Add and test encapsulation

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#33 In stanford-centaur/PyPantograph;

· lenianiva opened on Oct 18, 2024