Search results

[BUG] Lemmas are not extracted as a declaration

Status: Open.

#41 In augustepoiroux/LeanInteract;

· BorjaRequena opened on Mar 23, 2026

[BUG] Declarations are not delimited correctly when there are imports in the code

Status: Open.

#40 In augustepoiroux/LeanInteract;

· BorjaRequena opened on Mar 23, 2026

Mathlib search

Status: Open.

#39 In augustepoiroux/LeanInteract;

· catalin-hanga opened on Mar 3, 2026

How to use a local Lean project?

Status: Open.

#38 In augustepoiroux/LeanInteract;

· TitiSkywalker opened on Feb 15, 2026

[Documentation] When is it safe to have two processes spawn a LeanREPLConfig concurrently?

Status: Open.

#37 In augustepoiroux/LeanInteract;

· jonathan-laurent opened on Nov 19, 2025

[BUG] AutoLeanServer is not robust to crashes induced by stack overflows

Status: Open.

#36 In augustepoiroux/LeanInteract;

· jonathan-laurent opened on Nov 10, 2025