Skip to content

Pull requests: leanprover/theorem_proving_in_lean4

New pull request New
22 Open 104 Closed
22 Open 104 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

Typo in Chap. 7
#203 opened Dec 3, 2025 by makabaka1880 Loading…
Update InductiveTypes.lean
#201 opened Nov 30, 2025 by jouvelot Loading…
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…
Update Lean installation instructions link
#179 opened Nov 7, 2025 by VivienCabannes Loading…
1
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! no:milestone will show everything without a milestone.