leanprover/lean4

GitHub で見る

Lean 4 programming language and theorem prover

スター: 9.2k
フォーク: 990
オープンの初心者向け issue: 14
索引済み issue: 1k
平均マージ: 1日 15時間
マージ済み PR（30日）: 165

主要言語: Lean
ライセンス: Apache-2.0
最終 GitHub push: 2026年9月19日
最新の索引: 2026年9月20日
コントリビューションガイド: コントリビューションガイド
行動規範: 行動規範がありません
初心者向けラベル: help wanted

初心者向けすべて

オープンすべて

オープンの issue を 1,008 件索引しました

Std.Http.URI query encoding changes literal plus signs to spaces オープン

難易度 3/5 1〜2日初心者へのやさしさ 68/100

leanprover/lean4#15246 · 2026年9月21日に作成
RFC: safe withExclusive wrapper around isExclusiveUnsafe オープン

RFC

難易度 5/5 1週間以上初心者へのやさしさ 35/100

leanprover/lean4#15235 · 2026年9月20日に作成
`#print axioms` / `collectAxioms` under-reports axioms of imported inductives (in-progress sentinel cached by `exportedAxiomsExt`) オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 48/100

leanprover/lean4#15226 · 2026年9月19日に作成
`@[deprecated]` on a structure field projection does not warn when constructing the field オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 48/100

leanprover/lean4#15203 · 2026年9月17日に作成
`simpDiscrCtor?` is broken in the presence of non-type parameters オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 48/100

leanprover/lean4#15200 · 2026年9月17日に作成
`simp [...]` with a left arrow (`←`) on a simproc should error オープン

bug

難易度 2/5 1〜3時間初心者へのやさしさ 84/100

leanprover/lean4#15197 · 2026年9月17日に作成
`#guard_msgs` hides error messages from commands outside of it オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 45/100

leanprover/lean4#15196 · 2026年9月17日に作成
`bv_decide` fails with `unknown free variable '_fvar.126'` under certain contexts オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 48/100

leanprover/lean4#15195 · 2026年9月17日に作成
`Nat.shiftLeft` by 2^32 or more crashes Lean in `rfl`, `decide`, `simp`, `cbv`, `grind` and the compiler オープン

難易度 4/5 3〜5日初心者へのやさしさ 45/100

leanprover/lean4#15193 · 2026年9月17日に作成
Emscripten build passes `-pthread` unconditionally, ignoring `MULTI_THREAD=OFF` オープン

難易度 3/5 1〜2日初心者へのやさしさ 72/100

leanprover/lean4#15186 · コメント 1 件 · 2026年9月16日に作成
grind explodes on a simple example with `Array.range` オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 52/100

leanprover/lean4#15183 · 2026年9月16日に作成
(kernel) application type mismatch in `cbv` with `ite_true` オープン

bug

難易度 3/5 1〜2日初心者へのやさしさ 55/100

leanprover/lean4#15182 · 2026年9月16日に作成
MULTI_THREAD=OFF build fails: std::adopt_lock_t used in thread.h without including <mutex> オープン

難易度 2/5 1〜3時間初心者へのやさしさ 86/100

leanprover/lean4#15172 · コメント 1 件 · 2026年9月15日に作成
perf: reduce Nat.powMod kernel replay cost オープン

難易度 4/5 3〜5日初心者へのやさしさ 52/100

leanprover/lean4#15166 · 2026年9月15日に作成
RFC: structured log entries in Lake, and a JSON log format for `lake build` オープン

RFC

難易度 5/5 1週間以上初心者へのやさしさ 35/100

leanprover/lean4#15139 · コメント 2 件 · 2026年9月12日に作成
RFC: Support dependency in Verso docstrings オープン

RFC

難易度 5/5 1週間以上初心者へのやさしさ 45/100

leanprover/lean4#15137 · リアクション 2 件 · 2026年9月11日に作成
custom semantic highlighting appears only when source file is first edited オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 52/100

leanprover/lean4#15118 · コメント 6 件 · 2026年9月11日に作成
#guard_panic misclassifies ordinary errors as panics via a naive substring check, silently deleting the message log オープン

bug

難易度 3/5 1〜2日初心者へのやさしさ 68/100

leanprover/lean4#15117 · 2026年9月11日に作成
`#eval` of an `IO` action aborts `lean` (uncaught `lean::exception`, exit 134) when it reaches a non-`meta` import through a local definition オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 52/100

leanprover/lean4#15113 · コメント 2 件 · 2026年9月10日に作成
Linux: libleanshared.so exports a partial _Unwind_* ABI, breaking C++ exceptions inside FFI libraries built against libstdc++ オープン

難易度 4/5 3〜5日初心者へのやさしさ 45/100

leanprover/lean4#15112 · リアクション 1 件 · 2026年9月10日に作成
Missing goal state after `grind =>`, `sym =>` and `impossible by` オープン

bug

難易度 3/5 1〜2日初心者へのやさしさ 70/100

leanprover/lean4#15108 · コメント 1 件 · リアクション 2 件 · 2026年9月10日に作成
omega hits the recursion limit on a reflexive multiplication goal with an unused hypothesis オープン

bug

難易度 3/5 1〜2日初心者へのやさしさ 64/100

leanprover/lean4#15102 · 2026年9月9日に作成
`grind` failing to apply lemma if instance is not syntactically equal オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 55/100

leanprover/lean4#15082 · コメント 1 件 · 2026年9月9日に作成
RFC: use `Std.Refl`/`Std.Symm` instances in `rfl`/`symm` オープン

RFC

難易度 5/5 1週間以上初心者へのやさしさ 39/100

leanprover/lean4#15081 · リアクション 2 件 · 2026年9月9日に作成
`deriving instance CoeFun/CoeSort` generates opaque aux constant for reducible type synonyms オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 55/100

leanprover/lean4#15065 · コメント 1 件 · リアクション 3 件 · 2026年9月8日に作成
Std.Http minor cleanups オープン

RFC

難易度 4/5 3〜5日初心者へのやさしさ 35/100

leanprover/lean4#15051 · リアクション 1 件 · 2026年9月7日に作成
No `goalsAccomplished` message is produced for theorems generated using `elab` オープン

bug P-medium

難易度 3/5 1〜2日初心者へのやさしさ 72/100

leanprover/lean4#15044 · コメント 1 件 · 2026年9月6日に作成
Delaborator omits an instance binder's name when it is used only in a later binder's type オープン

P-medium

難易度 2/5 1〜3時間初心者へのやさしさ 78/100

leanprover/lean4#15037 · 2026年9月4日に作成
`pp.all` output does not round-trip when a local's type has `optParam`/`autoParam` binders オープン

P-low

難易度 4/5 3〜5日初心者へのやさしさ 55/100

leanprover/lean4#15035 · 2026年9月4日に作成
`Failed to find LCNF signature` reported to users where v4.20 gave the `noncomputable` hint オープン

P-low

難易度 4/5 3〜5日初心者へのやさしさ 45/100

leanprover/lean4#15034 · 2026年9月4日に作成
Compiler PANIC in `ExplicitBoxing` when `deriving Repr`/`BEq` over an `unsafe instance` オープン

P-medium

難易度 4/5 3〜5日初心者へのやさしさ 52/100

leanprover/lean4#15033 · コメント 1 件 · 2026年9月4日に作成
`Nat.lt` docstring オープン

P-low

難易度 1/5 1時間未満初心者へのやさしさ 85/100

leanprover/lean4#15014 · 2026年9月4日に作成
Very high CPU usage when making any edits at the top of a file オープン

bug P-medium

難易度 4/5 3〜5日初心者へのやさしさ 45/100

leanprover/lean4#15013 · コメント 4 件 · リアクション 3 件 · 2026年9月4日に作成
typecheck error sometimes escapes `first` オープン

bug P-medium

難易度 4/5 3〜5日初心者へのやさしさ 45/100

leanprover/lean4#15000 · リアクション 1 件 · 2026年9月2日に作成
stack overflow hangs instead of aborting when the fault lands inside the allocator オープン

bug P-medium

難易度 4/5 3〜5日初心者へのやさしさ 25/100

leanprover/lean4#14992 · 2026年9月1日に作成
olean loader: no-mmap fallback re-reads the entire file after the header probe オープン

bug P-low

難易度 3/5 1〜2日初心者へのやさしさ 72/100

leanprover/lean4#14991 · 2026年9月1日に作成
Private proof materializes a public equation theorem オープン

bug P-medium

難易度 4/5 3〜5日初心者へのやさしさ 45/100

leanprover/lean4#14986 · 2026年9月1日に作成
`subst` and `simp` reorder hypotheses when rewriting オープン

bug P-low

難易度 4/5 3〜5日初心者へのやさしさ 52/100

leanprover/lean4#14985 · リアクション 1 件 · 2026年9月1日に作成
Meta issue: Lean Kernel Logic renovation オープン

P-high

難易度 5/5 1週間以上初心者へのやさしさ 25/100

leanprover/lean4#14977 · コメント 1 件 · リアクション 9 件 · 2026年8月31日に作成
Unexpected compilation error "Could not find native implementation of external declaration" オープン

bug P-medium

難易度 4/5 3〜5日初心者へのやさしさ 52/100

leanprover/lean4#14975 · 2026年8月30日に作成
Emscripten libuv stub definitions do not match their declarations オープン

P-medium

難易度 2/5 1〜3時間初心者へのやさしさ 84/100

leanprover/lean4#14973 · コメント 1 件 · 2026年8月30日に作成
kernel rejects simp proof, dischargeEqnThmHypothesis not well behaving オープン

bug

難易度 4/5 3〜5日初心者へのやさしさ 46/100

leanprover/lean4#14961 · コメント 1 件 · 2026年8月29日に作成
deriving ToJson/FromJson generates ill-typed code for self-recursion in a non-first mutual member オープン

難易度 2/5 1〜3時間初心者へのやさしさ 85/100

leanprover/lean4#14958 · 2026年8月28日に作成
Cannot derive eq_def for an @[irreducible] well-founded definition オープン

bug P-low

難易度 4/5 3〜5日初心者へのやさしさ 45/100

leanprover/lean4#14957 · コメント 5 件 · 2026年8月28日に作成
Unification sees through type synonyms when checking instances' types オープン

bug

leanprover/lean4#14949 · 担当者 1 名 · 2026年8月28日に作成
RFC: Mutual inductives with heterogeneous universes オープン

RFC

難易度 5/5 1週間以上初心者へのやさしさ 25/100

leanprover/lean4#14944 · コメント 4 件 · 2026年8月27日に作成
`Std.Http`: `URI.Query` lookups compare percent-encoded bytes, which are not canonical オープン

bug

難易度 3/5 1〜2日初心者へのやさしさ 76/100

leanprover/lean4#14934 · リアクション 1 件 · 2026年8月26日に作成
RFC: Generalize Array.binSearch with partition-point-style API オープン

RFC

難易度 5/5 1週間以上初心者へのやさしさ 35/100

leanprover/lean4#14931 · 2026年8月26日に作成
simp still panics with appArg!/appFn! in the non-indexed rewriting path オープン

難易度 2/5 1〜3時間初心者へのやさしさ 82/100

leanprover/lean4#14930 · コメント 1 件 · 2026年8月25日に作成
Selectable.one + TCP.recvSelector retains RSS on repeated wait-for-read (not recv?) オープン

bug P-medium

難易度 4/5 3〜5日初心者へのやさしさ 48/100

leanprover/lean4#14924 · 2026年8月25日に作成

leanprover/lean4

新しい issue をメールで受け取る