Proprietario

leanprover

34 repository indicizzati · Vedi su GitHub

lean4
Lean 4 programming language and theorem prover

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

Lean · 709 stelle
elan
The Lean version manager

Rust · 637 stelle
verso
Lean documentation authoring tool

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

TypeScript · 313 stelle
theorem_proving_in_lean4
Theorem Proving in Lean 4

Lean · 272 stelle
comparator

Lean · 203 stelle
fp-lean
Functional Programming in Lean

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

Lean · 173 stelle
reference-manual
The Lean reference manual

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

Lean · 120 stelle
SampCert
SampCert : Verified Differential Privacy

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

Vue · 50 stelle
TensorLib
A verified tensor library in Lean

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

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

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

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

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

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

Lean · 31 stelle
14 altri repository si trovano su Vedi su GitHub

Adatte ai principianti Tutto

Aperta Tutte

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

Difficoltà 3/5 1-2 giorni Idoneità per principianti 68/100

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

dependency-incompatibility

Difficoltà 3/5 1-2 giorni Idoneità per principianti 45/100

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

RFC

Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

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

bug

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

leanprover/lean-eval-submissions#1739 · 1 commento · Aperta il 18/9/2026
minus function in GettingToKnow/DatatypesPatterns.lean doesn't work Aperta

Difficoltà 1/5 Meno di un'ora Idoneità per principianti 92/100

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

bug

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

bug

Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 68/100

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

bug

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

bug

Difficoltà 2/5 1-3 ore Idoneità per principianti 84/100

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

bug

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

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

bug

Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

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

Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

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

Difficoltà 3/5 1-2 giorni Idoneità per principianti 72/100

leanprover/lean4#15186 · 1 commento · Aperta il 16/9/2026
Unify treatment of temp directories. Aperta

Difficoltà 3/5 1-2 giorni Idoneità per principianti 68/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

leanprover/lean-workbench#140 · 1 commento · Aperta il 16/9/2026
grind explodes on a simple example with `Array.range` Aperta

bug

Difficoltà 4/5 3-5 giorni Idoneità per principianti 52/100

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

bug

Difficoltà 3/5 1-2 giorni Idoneità per principianti 55/100

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

Difficoltà 2/5 1-3 ore Idoneità per principianti 86/100

leanprover/lean4#15172 · 1 commento · Aperta il 15/9/2026
The "Rename Symbol" code action fails to account for constructor/destructor tags Aperta

bug

Difficoltà 3/5 1-2 giorni Idoneità per principianti 58/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 52/100

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

Difficoltà 5/5 Più di una settimana Idoneità per principianti 45/100

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

Difficoltà 3/5 1-2 giorni Idoneità per principianti 64/100

leanprover/lean-eval#637 · 1 reazione · Aperta il 13/9/2026
Should a checker reject a let type mismatch that disappears after substitution? Aperta

Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

leanprover/lean4export#48 · 1 commento · Aperta il 13/9/2026
Post-overhaul UX, performance, and cleanup triage Aperta

Difficoltà 5/5 Più di una settimana Idoneità per principianti 20/100

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

Difficoltà 2/5 1-3 ore Idoneità per principianti 68/100

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

Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

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

Difficoltà 2/5 1-3 ore Idoneità per principianti 70/100

leanprover/lean-beam#257 · Aperta il 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 Aperta

Difficoltà 4/5 3-5 giorni Idoneità per principianti 52/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 52/100

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

RFC

Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

leanprover/lean4#15139 · 2 commenti · Aperta il 12/9/2026
RFC: Support dependency in Verso docstrings Aperta

RFC

Difficoltà 5/5 Più di una settimana Idoneità per principianti 45/100

leanprover/lean4#15137 · 2 reazioni · Aperta il 11/9/2026
custom semantic highlighting appears only when source file is first edited Aperta

bug

Difficoltà 4/5 3-5 giorni Idoneità per principianti 52/100

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

bug

Difficoltà 3/5 1-2 giorni Idoneità per principianti 68/100

leanprover/lean4#15117 · Aperta il 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 Aperta

bug

Difficoltà 4/5 3-5 giorni Idoneità per principianti 52/100

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

Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

leanprover/lean4#15112 · 1 reazione · Aperta il 10/9/2026
Missing goal state after `grind =>`, `sym =>` and `impossible by` Aperta

bug

Difficoltà 3/5 1-2 giorni Idoneità per principianti 70/100

leanprover/lean4#15108 · 1 commento · 2 reazioni · Aperta il 10/9/2026
Is there an existing or planned HTML-to-Verso importer? Aperta

Difficoltà 5/5 Più di una settimana Idoneità per principianti 30/100

leanprover/verso#980 · 1 commento · Aperta il 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? Aperta

Difficoltà 4/5 3-5 giorni Idoneità per principianti 38/100

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

bug

Difficoltà 3/5 1-2 giorni Idoneità per principianti 64/100

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

bug

Difficoltà 4/5 3-5 giorni Idoneità per principianti 55/100

leanprover/lean4#15082 · 1 commento · Aperta il 9/9/2026
RFC: use `Std.Refl`/`Std.Symm` instances in `rfl`/`symm` Aperta

RFC

Difficoltà 5/5 Più di una settimana Idoneità per principianti 39/100

leanprover/lean4#15081 · 2 reazioni · Aperta il 9/9/2026
Deal with name collisions Aperta

Difficoltà 4/5 3-5 giorni Idoneità per principianti 38/100

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

bug

Difficoltà 4/5 3-5 giorni Idoneità per principianti 55/100

leanprover/lean4#15065 · 1 commento · 3 reazioni · Aperta il 8/9/2026
verso-literate attaches a declaration's docstring to a constant defined by one of its attributes Aperta

Difficoltà 3/5 1-2 giorni Idoneità per principianti 65/100

leanprover/verso#979 · Aperta il 7/9/2026
Std.Http minor cleanups Aperta

RFC

Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

leanprover/lean4#15051 · 1 reazione · Aperta il 7/9/2026
Open projects into a reasonable state Aperta

Difficoltà 3/5 1-2 giorni Idoneità per principianti 64/100

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

Difficoltà 3/5 1-2 giorni Idoneità per principianti 72/100

leanprover/elan#210 · Aperta il 6/9/2026

Vengono mostrati i 100 più recenti

Questa pagina elenca solo ciò che è stato indicizzato di recente. Il filtro avanzato contiene l'inventario completo, ristretto per linguaggio, difficoltà e durata.

Apri il filtro avanzato

leanprover

Vengono mostrati i 100 più recenti

Ricevi le nuove issue nella tua casella