オーナー

leanprover

索引済みのリポジトリ 34 件 · GitHub で見る

lean4
Lean 4 programming language and theorem prover

Lean · スター 9227 個
cslib
The Lean Computer Science Library (CSLib)

Lean · スター 709 個
elan
The Lean version manager

Rust · スター 637 個
verso
Lean documentation authoring tool

Lean · スター 384 個
vscode-lean4
VS Code extension for the Lean 4 programming language and theorem prover

TypeScript · スター 313 個
theorem_proving_in_lean4
Theorem Proving in Lean 4

Lean · スター 272 個
comparator

Lean · スター 203 個
fp-lean
Functional Programming in Lean

Lean · スター 192 個
doc-gen4
Document Generator for Lean 4

Lean · スター 173 個
reference-manual
The Lean reference manual

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

Lean · スター 120 個
SampCert
SampCert : Verified Differential Privacy

Lean · スター 105 個
reservoir
Package registry for Lean/Lake.

Vue · スター 50 個
TensorLib
A verified tensor library in Lean

Lean · スター 49 個
lean-eval
Comparator-based Lean formal mathematics eval

Lean · スター 46 個
lean-action
GitHub action for standard CI in Lean projects

Shell · スター 45 個
lean4export
Plain-text declaration export for Lean 4

Lean · スター 40 個
verso-templates
Templates for getting started with Verso

Lean · スター 38 個
human-eval-lean
Hand-written verified Lean solutions for the HumanEval benchmark

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

Lean · スター 31 個
ほか 14 件のリポジトリは GitHub で見るにあります

初心者向けすべて

オープンすべて

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

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

leanprover/lean4#15246 · 2026年9月21日に作成
Bumping mathlib to d8307f8 would break the build オープン

dependency-incompatibility

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

leanprover/cslib#928 · 2026年9月20日に作成
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日に作成
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日に作成
Tracking-issue option on statement directives (`issue := N`), alongside `pr_url` オープン

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

leanprover/verso-blueprint#463 · コメント 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日に作成
`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日に作成
There's needs to be a way to submit with much higher memory limit オープン

難易度 5/5 1週間以上初心者へのやさしさ 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 · 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 1週間以上初心者へのやさしさ 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 件 · 2026年9月13日に作成
Should a checker reject a let type mismatch that disappears after substitution? オープン

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

leanprover/lean4export#48 · コメント 1 件 · 2026年9月13日に作成
Post-overhaul UX, performance, and cleanup triage オープン

難易度 5/5 1週間以上初心者へのやさしさ 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 1週間以上初心者へのやさしさ 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 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日に作成
Is there an existing or planned HTML-to-Verso importer? オープン

難易度 5/5 1週間以上初心者へのやさしさ 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 1週間以上初心者へのやさしさ 39/100

leanprover/lean4#15081 · リアクション 2 件 · 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 件 · 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 件 · 2026年9月7日に作成
Open projects into a reasonable state オープン

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

leanprover/lean-workbench#130 · 2026年9月6日に作成
elan-init --default-toolchain records the default but never installs it (exits 0 with no toolchain on disk) オープン

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

leanprover/elan#210 · 2026年9月6日に作成

leanprover

最新の 100 件のみ表示しています

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