Owner

leanprover

已索引 34 个仓库 · 在 GitHub 查看

lean4
Lean 4 programming language and theorem prover

Lean · 9227 个 star
cslib
The Lean Computer Science Library (CSLib)

Lean · 709 个 star
elan
The Lean version manager

Rust · 637 个 star
verso
Lean documentation authoring tool

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

TypeScript · 313 个 star
theorem_proving_in_lean4
Theorem Proving in Lean 4

Lean · 272 个 star
comparator

Lean · 203 个 star
fp-lean
Functional Programming in Lean

Lean · 192 个 star
doc-gen4
Document Generator for Lean 4

Lean · 173 个 star
reference-manual
The Lean reference manual

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

Lean · 120 个 star
SampCert
SampCert : Verified Differential Privacy

Lean · 105 个 star
reservoir
Package registry for Lean/Lake.

Vue · 50 个 star
TensorLib
A verified tensor library in Lean

Lean · 49 个 star
lean-eval
Comparator-based Lean formal mathematics eval

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

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

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

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

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

Lean · 31 个 star
还有 14 个仓库在在 GitHub 查看

适合新手全部

未关闭全部

Efficient arbitrary-precision trailing-zero counting for Nat and Int 未关闭

leanprover/lean4#15264 · 已指派 1 人 · 2026年9月22日创建
grind with BitVec.allOnes is broken by replacing variable with literal constant 未关闭

bug

难度 4/5 3-5 天新手友好度 52/100

leanprover/lean4#15261 · 2026年9月22日创建
grind_hom does not recognize arithmetic properties of constant bitmasks 未关闭

bug

难度 4/5 3-5 天新手友好度 50/100

leanprover/lean4#15260 · 2026年9月21日创建
Lean kernel replay rejects any theorem whose proof reduces a string literal 未关闭

难度 4/5 3-5 天新手友好度 52/100

leanprover/comparator#93 · 2026年9月21日创建
Missing constant folding rules for `toUIntX` functions 未关闭

bug

难度 2/5 1-3 小时新手友好度 84/100

leanprover/lean4#15255 · 2026年9月21日创建
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 一周以上新手友好度 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 · 1 条评论 · 2026年9月19日创建
OAuth callback returns 503 state_unavailable after successful GitHub authorization (reproducible, 2026-09-18 ~04:05–04:25 UTC) 未关闭

难度 4/5 3-5 天新手友好度 48/100

leanprover/lean-eval-submissions#1739 · 1 条评论 · 2026年9月18日创建
minus function in GettingToKnow/DatatypesPatterns.lean doesn't work 未关闭

难度 1/5 1 小时以内新手友好度 92/100

leanprover/fp-lean#301 · 2026年9月17日创建
`@[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日创建
Completion popup reopens after Esc in Lean files; caused by default quickSuggestionsDelay of 200 未关闭

bug

难度 2/5 1-3 小时新手友好度 72/100

leanprover/vscode-lean4#800 · 1 条评论 · 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日创建
`#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 · 1 个 reaction · 2026年9月17日创建
There's needs to be a way to submit with much higher memory limit 未关闭

难度 5/5 一周以上新手友好度 35/100

leanprover/lean-eval#642 · 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日创建
Unify treatment of temp directories. 未关闭

难度 3/5 1-2 天新手友好度 68/100

leanprover/lean-workbench#142 · 2026年9月16日创建
Move `_file` to publications origin 未关闭

难度 4/5 3-5 天新手友好度 35/100

leanprover/lean-workbench#140 · 1 条评论 · 2026年9月16日创建
grind explodes on a simple example with `Array.range` 未关闭

bug

难度 4/5 3-5 天新手友好度 52/100

leanprover/lean4#15183 · 1 条评论 · 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日创建
The "Rename Symbol" code action fails to account for constructor/destructor tags 未关闭

bug

难度 3/5 1-2 天新手友好度 58/100

leanprover/vscode-lean4#799 · 2026年9月15日创建
perf: reduce Nat.powMod kernel replay cost 未关闭

难度 4/5 3-5 天新手友好度 52/100

leanprover/lean4#15166 · 2026年9月15日创建
@[blueprint] behavior depends on imports 未关闭

难度 5/5 一周以上新手友好度 45/100

leanprover/verso-blueprint#462 · 2026年9月14日创建
New submission page is broken 未关闭

难度 3/5 1-2 天新手友好度 64/100

leanprover/lean-eval#637 · 1 个 reaction · 2026年9月13日创建
Should a checker reject a let type mismatch that disappears after substitution? 未关闭

难度 5/5 一周以上新手友好度 35/100

leanprover/lean4export#48 · 1 条评论 · 2026年9月13日创建
Post-overhaul UX, performance, and cleanup triage 未关闭

难度 5/5 一周以上新手友好度 20/100

leanprover/lean-eval#634 · 2026年9月13日创建
Axioms and Computation: is "virtual machine" still the right term? 未关闭

难度 2/5 1-3 小时新手友好度 68/100

leanprover/theorem_proving_in_lean4#233 · 2026年9月13日创建
Follow up on transport, test setup, and documentation review 未关闭

难度 5/5 一周以上新手友好度 25/100

leanprover/subverso#240 · 2026年9月12日创建
Docs: lean_sync runs setup-file and builds stale imports; the daemon pins the toolchain under .beam 未关闭

难度 2/5 1-3 小时新手友好度 70/100

leanprover/lean-beam#257 · 2026年9月12日创建
An external Lake build never clears a dependency's needsSave; the sync barrier then refuses the importer and the recovery plan points at save 未关闭

难度 4/5 3-5 天新手友好度 52/100

leanprover/lean-beam#256 · 2026年9月12日创建
lean_save hangs to the client idle timeout instead of returning saveUnsupportedSetup in a package with batch-only moreLeanArgs 未关闭

难度 4/5 3-5 天新手友好度 52/100

leanprover/lean-beam#255 · 2026年9月12日创建
RFC: structured log entries in Lake, and a JSON log format for `lake build` 未关闭

RFC

难度 5/5 一周以上新手友好度 35/100

leanprover/lean4#15139 · 2 条评论 · 2026年9月12日创建
RFC: Support dependency in Verso docstrings 未关闭

RFC

难度 5/5 一周以上新手友好度 45/100

leanprover/lean4#15137 · 2 个 reaction · 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 个 reaction · 2026年9月10日创建
Missing goal state after `grind =>`, `sym =>` and `impossible by` 未关闭

bug

难度 3/5 1-2 天新手友好度 70/100

leanprover/lean4#15108 · 1 条评论 · 2 个 reaction · 2026年9月10日创建
Is there an existing or planned HTML-to-Verso importer? 未关闭

难度 5/5 一周以上新手友好度 30/100

leanprover/verso#980 · 1 条评论 · 2026年9月10日创建
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? 未关闭

难度 4/5 3-5 天新手友好度 38/100

leanprover/lean-eval-submissions#1697 · 1 条评论 · 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 一周以上新手友好度 39/100

leanprover/lean4#15081 · 2 个 reaction · 2026年9月9日创建
Deal with name collisions 未关闭

难度 4/5 3-5 天新手友好度 38/100

leanprover/lean-workbench#132 · 1 条评论 · 2026年9月8日创建
`deriving instance CoeFun/CoeSort` generates opaque aux constant for reducible type synonyms 未关闭

bug

难度 4/5 3-5 天新手友好度 55/100

leanprover/lean4#15065 · 1 条评论 · 3 个 reaction · 2026年9月8日创建
verso-literate attaches a declaration's docstring to a constant defined by one of its attributes 未关闭

难度 3/5 1-2 天新手友好度 65/100

leanprover/verso#979 · 2026年9月7日创建
Std.Http minor cleanups 未关闭

RFC

难度 4/5 3-5 天新手友好度 35/100

leanprover/lean4#15051 · 1 个 reaction · 2026年9月7日创建

只显示最新的 100 条

这个页面只列出最近收录的部分。完整清单在高级筛选里，可以按语言、难度和预计耗时筛选。

前往高级筛选

leanprover

只显示最新的 100 条

把新 issue 发到你的邮箱