Skip to content

Pull requests: leanprover/cslib

New pull request New
114 Open 597 Closed
114 Open 597 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

refactor(MultiTapeTM): Make the deterministic machine a nondeterministic one
#821 opened Aug 19, 2026 by barni120400 Loading…
feat(MultiTapeTM): Nondeterministic multi-tape Turing machines
#820 opened Aug 19, 2026 by barni120400 Loading…
refactor(MultiTapeTM): Put the output tape into the configuration
#819 opened Aug 19, 2026 by barni120400 Loading…
3
feat(MultiTapeTM): Normal form for acceptor-style TMs
#817 opened Aug 18, 2026 by crei Collaborator Loading…
feat(MultiTapeTM): halting-time, output-length, and visited-position lemmas for multi-tape TMs
#816 opened Aug 18, 2026 by SamuelSchlesinger Collaborator Loading…
3
refactor: abbrev open'/close
#815 opened Aug 18, 2026 by lengyijun Contributor Loading…
8
chore: remove FinFun, a duplicate of Mathlib's Finsupp
#814 opened Aug 17, 2026 by SamuelSchlesinger Collaborator Loading…
3
refactor(Crypto): replace bespoke constructions with Mathlib abstractions
#813 opened Aug 17, 2026 by SamuelSchlesinger Collaborator Loading…
7
feat: graph definitions (#Attempts 3)
#810 opened Aug 17, 2026 by sorrachai Collaborator Loading…
31
feat(Crypto/Primitives/ECC): Edwards Curves
#809 opened Aug 17, 2026 by chris-anto-froeschl Contributor Loading…
13
feat(governance): add Christian Reitwiessner to reviewers
#808 opened Aug 17, 2026 by fmontesi Collaborator Loading…
feat: FullEta.steps_fv
#807 opened Aug 16, 2026 by lengyijun Contributor Loading…
refactor(LTS): convert LTS.Execution from a Prop to a structure
#806 opened Aug 16, 2026 by ctchou Collaborator Loading…
@chenson2018
1
feat: demo DFS for graph without explicit adjList structure
#805 opened Aug 15, 2026 by Shreyas4991 Contributor • Draft
feat: demo DFS with mathlib Graph and TimeM
#804 opened Aug 15, 2026 by Shreyas4991 Contributor • Draft
feat(PFunctor): Add API of basic constructions
#803 opened Aug 15, 2026 by dtumad Loading…
7
feat(MultiTapeTM): Nondeterministic multi-tape Turing machines
#802 opened Aug 14, 2026 by barni120400 Loading…
1
feat: Add BetaAt uniqueness, FV preservation, and left redex-count bound
#800 opened Aug 14, 2026 by lengyijun Contributor Loading…
2
feat(ModalLogic+Congruence): modal reasoning for Lean
#799 opened Aug 14, 2026 by fmontesi Collaborator Loading…
@arademaker @thomaskwaring
38
refactor(LocallyNameless): Extract depth into a dedicated module
#798 opened Aug 14, 2026 by lengyijun Contributor Loading…
3
refactor: .trans => .head/.tail
#797 opened Aug 13, 2026 by lengyijun Contributor Loading…
1
test(LambdaCalculus): port the lambda-n-ways normalization corpus
#791 opened Aug 10, 2026 by korbonits Loading…
1
feat(ModalLogic): IsAxiom and axiom L (Löb's theorem for modal logic)
#788 opened Aug 10, 2026 by fmontesi Collaborator Loading…
@arademaker @SamuelSchlesinger @thomaskwaring
refactor: Replace ↔ with = in LcAt.lean
#787 opened Aug 9, 2026 by lengyijun Contributor Loading…
feat(Crypto/Systems): Elligator 1, Theorem 1 and Definition 2
#783 opened Aug 8, 2026 by chris-anto-froeschl Contributor Loading…
16
ProTip! Exclude everything labeled bug with -label:bug.