Propietario

leanprover

34 repositorios indexados · Ver en GitHub

lean4
Lean 4 programming language and theorem prover

Lean · 9227 estrellas
cslib
The Lean Computer Science Library (CSLib)

Lean · 709 estrellas
elan
The Lean version manager

Rust · 637 estrellas
verso
Lean documentation authoring tool

Lean · 384 estrellas
vscode-lean4
VS Code extension for the Lean 4 programming language and theorem prover

TypeScript · 313 estrellas
theorem_proving_in_lean4
Theorem Proving in Lean 4

Lean · 272 estrellas
comparator

Lean · 203 estrellas
fp-lean
Functional Programming in Lean

Lean · 192 estrellas
doc-gen4
Document Generator for Lean 4

Lean · 173 estrellas
reference-manual
The Lean reference manual

Lean · 129 estrellas
lean4-cli
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

Lean · 120 estrellas
SampCert
SampCert : Verified Differential Privacy

Lean · 105 estrellas
reservoir
Package registry for Lean/Lake.

Vue · 50 estrellas
TensorLib
A verified tensor library in Lean

Lean · 49 estrellas
lean-eval
Comparator-based Lean formal mathematics eval

Lean · 46 estrellas
lean-action
GitHub action for standard CI in Lean projects

Shell · 45 estrellas
lean4export
Plain-text declaration export for Lean 4

Lean · 40 estrellas
verso-templates
Templates for getting started with Verso

Lean · 38 estrellas
human-eval-lean
Hand-written verified Lean solutions for the HumanEval benchmark

Lean · 31 estrellas
lean-beam
Claude/Codex skill and local workflow layer for efficient interaction with Lean 4 and Monte-Carlo Tree Search.

Lean · 31 estrellas
14 repositorios más están en Ver en GitHub

Para principiantes Todo

Abierto Todos

Std.Http.URI query encoding changes literal plus signs to spaces Abierto

Dificultad 3/5 1-2 días Aptitud para principiantes 68/100

leanprover/lean4#15246 · Abierto el 21/9/2026
Bumping mathlib to d8307f8 would break the build Abierto

dependency-incompatibility

Dificultad 3/5 1-2 días Aptitud para principiantes 45/100

leanprover/cslib#928 · Abierto el 20/9/2026
RFC: safe withExclusive wrapper around isExclusiveUnsafe Abierto

RFC

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

leanprover/lean4#15235 · Abierto el 20/9/2026
`#print axioms` / `collectAxioms` under-reports axioms of imported inductives (in-progress sentinel cached by `exportedAxiomsExt`) Abierto

bug

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

leanprover/lean4#15226 · Abierto el 19/9/2026
OAuth callback returns 503 state_unavailable after successful GitHub authorization (reproducible, 2026-09-18 ~04:05–04:25 UTC) Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

leanprover/lean-eval-submissions#1739 · 1 comentario · Abierto el 18/9/2026
minus function in GettingToKnow/DatatypesPatterns.lean doesn't work Abierto

Dificultad 1/5 Menos de una hora Aptitud para principiantes 92/100

leanprover/fp-lean#301 · Abierto el 17/9/2026
`@[deprecated]` on a structure field projection does not warn when constructing the field Abierto

bug

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

leanprover/lean4#15203 · Abierto el 17/9/2026
Completion popup reopens after Esc in Lean files; caused by default quickSuggestionsDelay of 200 Abierto

bug

Dificultad 2/5 1-3 horas Aptitud para principiantes 72/100

leanprover/vscode-lean4#800 · 1 comentario · Abierto el 17/9/2026
Tracking-issue option on statement directives (`issue := N`), alongside `pr_url` Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 68/100

leanprover/verso-blueprint#463 · 1 comentario · Abierto el 17/9/2026
`simpDiscrCtor?` is broken in the presence of non-type parameters Abierto

bug

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

leanprover/lean4#15200 · Abierto el 17/9/2026
`simp [...]` with a left arrow (`←`) on a simproc should error Abierto

bug

Dificultad 2/5 1-3 horas Aptitud para principiantes 84/100

leanprover/lean4#15197 · Abierto el 17/9/2026
`#guard_msgs` hides error messages from commands outside of it Abierto

bug

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

leanprover/lean4#15196 · Abierto el 17/9/2026
`bv_decide` fails with `unknown free variable '_fvar.126'` under certain contexts Abierto

bug

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

leanprover/lean4#15195 · Abierto el 17/9/2026
`Nat.shiftLeft` by 2^32 or more crashes Lean in `rfl`, `decide`, `simp`, `cbv`, `grind` and the compiler Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

leanprover/lean4#15193 · Abierto el 17/9/2026
There's needs to be a way to submit with much higher memory limit Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

leanprover/lean-eval#642 · Abierto el 17/9/2026
Emscripten build passes `-pthread` unconditionally, ignoring `MULTI_THREAD=OFF` Abierto

Dificultad 3/5 1-2 días Aptitud para principiantes 72/100

leanprover/lean4#15186 · 1 comentario · Abierto el 16/9/2026
Unify treatment of temp directories. Abierto

Dificultad 3/5 1-2 días Aptitud para principiantes 68/100

leanprover/lean-workbench#142 · Abierto el 16/9/2026
Move `_file` to publications origin Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

leanprover/lean-workbench#140 · 1 comentario · Abierto el 16/9/2026
grind explodes on a simple example with `Array.range` Abierto

bug

Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

leanprover/lean4#15183 · Abierto el 16/9/2026
(kernel) application type mismatch in `cbv` with `ite_true` Abierto

bug

Dificultad 3/5 1-2 días Aptitud para principiantes 55/100

leanprover/lean4#15182 · Abierto el 16/9/2026
MULTI_THREAD=OFF build fails: std::adopt_lock_t used in thread.h without including <mutex> Abierto

Dificultad 2/5 1-3 horas Aptitud para principiantes 86/100

leanprover/lean4#15172 · 1 comentario · Abierto el 15/9/2026
The "Rename Symbol" code action fails to account for constructor/destructor tags Abierto

bug

Dificultad 3/5 1-2 días Aptitud para principiantes 58/100

leanprover/vscode-lean4#799 · Abierto el 15/9/2026
perf: reduce Nat.powMod kernel replay cost Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

leanprover/lean4#15166 · Abierto el 15/9/2026
@[blueprint] behavior depends on imports Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 45/100

leanprover/verso-blueprint#462 · Abierto el 14/9/2026
New submission page is broken Abierto

Dificultad 3/5 1-2 días Aptitud para principiantes 64/100

leanprover/lean-eval#637 · 1 reacción · Abierto el 13/9/2026
Should a checker reject a let type mismatch that disappears after substitution? Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

leanprover/lean4export#48 · 1 comentario · Abierto el 13/9/2026
Post-overhaul UX, performance, and cleanup triage Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 20/100

leanprover/lean-eval#634 · Abierto el 13/9/2026
Axioms and Computation: is "virtual machine" still the right term? Abierto

Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100

leanprover/theorem_proving_in_lean4#233 · Abierto el 13/9/2026
Follow up on transport, test setup, and documentation review Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

leanprover/subverso#240 · Abierto el 12/9/2026
Docs: lean_sync runs setup-file and builds stale imports; the daemon pins the toolchain under .beam Abierto

Dificultad 2/5 1-3 horas Aptitud para principiantes 70/100

leanprover/lean-beam#257 · Abierto el 12/9/2026
An external Lake build never clears a dependency's needsSave; the sync barrier then refuses the importer and the recovery plan points at save Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

leanprover/lean-beam#256 · Abierto el 12/9/2026
lean_save hangs to the client idle timeout instead of returning saveUnsupportedSetup in a package with batch-only moreLeanArgs Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

leanprover/lean-beam#255 · Abierto el 12/9/2026
RFC: structured log entries in Lake, and a JSON log format for `lake build` Abierto

RFC

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

leanprover/lean4#15139 · 2 comentarios · Abierto el 12/9/2026
RFC: Support dependency in Verso docstrings Abierto

RFC

Dificultad 5/5 Más de una semana Aptitud para principiantes 45/100

leanprover/lean4#15137 · 2 reacciones · Abierto el 11/9/2026
custom semantic highlighting appears only when source file is first edited Abierto

bug

Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

leanprover/lean4#15118 · 6 comentarios · Abierto el 11/9/2026
#guard_panic misclassifies ordinary errors as panics via a naive substring check, silently deleting the message log Abierto

bug

Dificultad 3/5 1-2 días Aptitud para principiantes 68/100

leanprover/lean4#15117 · Abierto el 11/9/2026
`#eval` of an `IO` action aborts `lean` (uncaught `lean::exception`, exit 134) when it reaches a non-`meta` import through a local definition Abierto

bug

Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

leanprover/lean4#15113 · 2 comentarios · Abierto el 10/9/2026
Linux: libleanshared.so exports a partial _Unwind_* ABI, breaking C++ exceptions inside FFI libraries built against libstdc++ Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

leanprover/lean4#15112 · 1 reacción · Abierto el 10/9/2026
Missing goal state after `grind =>`, `sym =>` and `impossible by` Abierto

bug

Dificultad 3/5 1-2 días Aptitud para principiantes 70/100

leanprover/lean4#15108 · 1 comentario · 2 reacciones · Abierto el 10/9/2026
Is there an existing or planned HTML-to-Verso importer? Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 30/100

leanprover/verso#980 · 1 comentario · Abierto el 10/9/2026
Kernel-heavy submissions: 360-min job with single-threaded nanoda replay caps `decide +kernel` work at ~10 CPU-h — is a larger budget or parallel replay possible? Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 38/100

leanprover/lean-eval-submissions#1697 · 1 comentario · Abierto el 10/9/2026
omega hits the recursion limit on a reflexive multiplication goal with an unused hypothesis Abierto

bug

Dificultad 3/5 1-2 días Aptitud para principiantes 64/100

leanprover/lean4#15102 · Abierto el 9/9/2026
`grind` failing to apply lemma if instance is not syntactically equal Abierto

bug

Dificultad 4/5 3-5 días Aptitud para principiantes 55/100

leanprover/lean4#15082 · 1 comentario · Abierto el 9/9/2026
RFC: use `Std.Refl`/`Std.Symm` instances in `rfl`/`symm` Abierto

RFC

Dificultad 5/5 Más de una semana Aptitud para principiantes 39/100

leanprover/lean4#15081 · 2 reacciones · Abierto el 9/9/2026
Deal with name collisions Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 38/100

leanprover/lean-workbench#132 · 1 comentario · Abierto el 8/9/2026
`deriving instance CoeFun/CoeSort` generates opaque aux constant for reducible type synonyms Abierto

bug

Dificultad 4/5 3-5 días Aptitud para principiantes 55/100

leanprover/lean4#15065 · 1 comentario · 3 reacciones · Abierto el 8/9/2026
verso-literate attaches a declaration's docstring to a constant defined by one of its attributes Abierto

Dificultad 3/5 1-2 días Aptitud para principiantes 65/100

leanprover/verso#979 · Abierto el 7/9/2026
Std.Http minor cleanups Abierto

RFC

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

leanprover/lean4#15051 · 1 reacción · Abierto el 7/9/2026
Open projects into a reasonable state Abierto

Dificultad 3/5 1-2 días Aptitud para principiantes 64/100

leanprover/lean-workbench#130 · Abierto el 6/9/2026
elan-init --default-toolchain records the default but never installs it (exits 0 with no toolchain on disk) Abierto

Dificultad 3/5 1-2 días Aptitud para principiantes 72/100

leanprover/elan#210 · Abierto el 6/9/2026

Mostrando los 100 más recientes

Esta página solo lista lo indexado más recientemente. El filtro avanzado tiene el inventario completo, acotado por lenguaje, dificultad y duración.

Abrir el filtro avanzado

leanprover

Mostrando los 100 más recientes

Recibe los nuevos issues en tu correo