leanprover/lean4

Lean 4 programming language and theorem prover

Stelle: 9.2k
Fork: 990
Issue aperte per principianti: 13
Issue indicizzate: 1k
Merge medio: 1g 15h
PR unite (30g): 185

Lingua principale: Lean
Licenza: Apache-2.0
Ultimo push su GitHub: 19/9/2026
Ultima indicizzazione: 20/9/2026
Guida per i contributori: Guida per i contributori
Codice di condotta: Nessun codice di condotta
Label per principianti: help wanted

Adatte ai principianti Tutto

Aperta Tutte

Type ascription with autoParam under ∀ᵐ times out Aperta

bug

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

leanprover/lean4#15284 · 1 commento · Aperta il 23/9/2026
feat: a way to build a project inside `lake check`'s sandbox without checking it Aperta

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

leanprover/lean4#15282 · Aperta il 23/9/2026
feat: `lake check --allow-sorry`, to permit `sorryAx` in in-progress projects Aperta

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

leanprover/lean4#15281 · Aperta il 23/9/2026
Efficient arbitrary-precision trailing-zero counting for Nat and Int Aperta

leanprover/lean4#15264 · 1 assegnatario · Aperta il 22/9/2026
grind with BitVec.allOnes is broken by replacing variable with literal constant Aperta

bug

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

leanprover/lean4#15261 · 2 commenti · Aperta il 22/9/2026
grind_hom does not recognize arithmetic properties of constant bitmasks Aperta

bug

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

leanprover/lean4#15260 · 2 reazioni · Aperta il 21/9/2026
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
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 · 1 commento · 1 reazione · Aperta il 19/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
`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
`#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 · 1 reazione · 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
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 · 1 commento · 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
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
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
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 commento · 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
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
`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
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
No `goalsAccomplished` message is produced for theorems generated using `elab` Aperta

bug P-medium

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

leanprover/lean4#15044 · 1 commento · Aperta il 6/9/2026
Delaborator omits an instance binder's name when it is used only in a later binder's type Aperta

P-medium

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

leanprover/lean4#15037 · Aperta il 4/9/2026
`pp.all` output does not round-trip when a local's type has `optParam`/`autoParam` binders Aperta

P-low

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

leanprover/lean4#15035 · Aperta il 4/9/2026
`Failed to find LCNF signature` reported to users where v4.20 gave the `noncomputable` hint Aperta

P-low

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

leanprover/lean4#15034 · Aperta il 4/9/2026
Compiler PANIC in `ExplicitBoxing` when `deriving Repr`/`BEq` over an `unsafe instance` Aperta

P-medium

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

leanprover/lean4#15033 · 1 commento · Aperta il 4/9/2026
`Nat.lt` docstring Aperta

P-low

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

leanprover/lean4#15014 · Aperta il 4/9/2026
Very high CPU usage when making any edits at the top of a file Aperta

bug P-medium

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

leanprover/lean4#15013 · 4 commenti · 4 reazioni · Aperta il 4/9/2026
typecheck error sometimes escapes `first` Aperta

bug P-medium

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

leanprover/lean4#15000 · 1 reazione · Aperta il 2/9/2026
stack overflow hangs instead of aborting when the fault lands inside the allocator Aperta

bug P-medium

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

leanprover/lean4#14992 · Aperta il 1/9/2026
olean loader: no-mmap fallback re-reads the entire file after the header probe Aperta

bug P-low

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

leanprover/lean4#14991 · Aperta il 1/9/2026
Private proof materializes a public equation theorem Aperta

bug P-medium

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

leanprover/lean4#14986 · Aperta il 1/9/2026
`subst` and `simp` reorder hypotheses when rewriting Aperta

bug P-low

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

leanprover/lean4#14985 · 1 reazione · Aperta il 1/9/2026
Meta issue: Lean Kernel Logic renovation Aperta

P-high

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

leanprover/lean4#14977 · 1 commento · 9 reazioni · Aperta il 31/8/2026
Unexpected compilation error "Could not find native implementation of external declaration" Aperta

bug P-medium

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

leanprover/lean4#14975 · Aperta il 30/8/2026
Emscripten libuv stub definitions do not match their declarations Aperta

P-medium

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

leanprover/lean4#14973 · 1 commento · Aperta il 30/8/2026
kernel rejects simp proof, dischargeEqnThmHypothesis not well behaving Aperta

bug

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

leanprover/lean4#14961 · 1 commento · Aperta il 29/8/2026
deriving ToJson/FromJson generates ill-typed code for self-recursion in a non-first mutual member Aperta

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

leanprover/lean4#14958 · Aperta il 28/8/2026
Cannot derive eq_def for an @[irreducible] well-founded definition Aperta

bug P-low

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

leanprover/lean4#14957 · 5 commenti · Aperta il 28/8/2026
Unification sees through type synonyms when checking instances' types Aperta

bug

leanprover/lean4#14949 · 1 assegnatario · Aperta il 28/8/2026
RFC: Mutual inductives with heterogeneous universes Aperta

RFC

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

leanprover/lean4#14944 · 4 commenti · Aperta il 27/8/2026
`Std.Http`: `URI.Query` lookups compare percent-encoded bytes, which are not canonical Aperta

bug

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

leanprover/lean4#14934 · 1 reazione · Aperta il 26/8/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/lean4

Vengono mostrati i 100 più recenti

Ricevi le nuove issue nella tua casella