Skip to content

Pull requests: leanprover/theorem_proving_in_lean4

New pull request New
22 Open 109 Closed
22 Open 109 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Fix rw explanation in Tactics chapter
#217 opened Feb 24, 2026 by freizl Loading…
Chapter 8.6 Functional Induction - simp ack is unsued
#216 opened Jan 26, 2026 by rubydusa Loading…
fix(examples): preserve newlines in copied code snippets
#213 opened Dec 24, 2025 by exekis Loading…
1
Update DependentTypeTheory.lean and Tactics.lean
#195 opened Nov 19, 2025 by jouvelot Loading…
Update Intro.lean
#194 opened Nov 19, 2025 by jouvelot Loading…
Add missing "set_option linter.unusedVariables false"
#174 opened Oct 5, 2025 by ozgurakgun Loading…
Update wording in DependentTypeTheory.lean
#173 opened Sep 28, 2025 by ozgurakgun Loading…
Update Example Code for Feature Change in 'variable' visibility
#154 opened Apr 22, 2025 by yanggao04 Loading…
Rust note, typo fix
#144 opened Dec 23, 2024 by mhartl Loading…
fix: missing comma in ch9.Objects
#143 opened Dec 12, 2024 by dmyTRUEk Loading…
Deletes repeated section Local Recursive Definitions in induction_and_recursion.md
#135 opened Oct 31, 2024 by javierlcontreras Loading…
Use eval! to evaluate functions that use sorry.
#133 opened Oct 23, 2024 by lcrh Loading…
1
small but unpleasant typo
#122 opened Jul 14, 2024 by stepanholub Loading…
add pdf version and build instructions
#119 opened Jun 13, 2024 by ocramz Loading…
fix: clarify that Lean's core library uses classical logic
#117 opened May 27, 2024 by avigad Loading…
Suggestions for clarity
#114 opened May 6, 2024 by turibe Loading…
6
fix: Update examples to work with latest Lean nightly
#107 opened Mar 1, 2024 by david-christiansen Loading…
5
Remove duplicated section.
#94 opened Jan 10, 2024 by DeVilhena-Paulo Loading…
Fix typo in tactics.md
#84 opened Nov 16, 2023 by deepimpactmir Loading…
1
Fix creation of Trans instance in calculational proof section
#83 opened Oct 25, 2023 by Shiney Loading…
Update type_classes.md
#77 opened Oct 1, 2023 by Erotemic Loading…
Update quantifiers_and_equality.md
#76 opened Sep 15, 2023 by JiechengZhao Loading…
ProTip! Follow long discussions with comments:>50.