Skip to content

Pull requests: leanprover/cslib

New pull request New
109 Open 595 Closed
109 Open 595 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

chore: remove FinFun, a duplicate of Mathlib's Finsupp
#814 opened Aug 17, 2026 by SamuelSchlesinger Collaborator Loading…
1
refactor(Crypto): replace bespoke constructions with Mathlib abstractions
#813 opened Aug 17, 2026 by SamuelSchlesinger Collaborator Loading…
feat: graph definitions (#Attempts 3)
#810 opened Aug 17, 2026 by sorrachai Collaborator Loading…
22
feat(Crypto/Primitives/ECC): Edwards Curves
#809 opened Aug 17, 2026 by chris-anto-froeschl Contributor Loading…
8
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…
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
28
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
feat(CFG): Verified implementation of Kildall's algorithm
#782 opened Aug 7, 2026 by quartztz • Draft
9
feat(Data): Results about RelatesInSteps with bounds on the reachable set
#779 opened Aug 6, 2026 by crei Collaborator Loading…
14
feat(MultitapeTM): Prove an exponential upper bound in the number of configurations reachable in bounded space
#772 opened Aug 3, 2026 by crei Collaborator Loading…
feat(CCS): notation for CCS process calculi
#771 opened Aug 3, 2026 by fmontesi Collaborator Loading…
feat(Algorithms): comparison sort lower bound via decision-tree induction
#770 opened Aug 3, 2026 by SamuelSchlesinger Collaborator Loading…
7
feat(MultiTapeTM): Prove time upper-bounds for space-bounded classes
#767 opened Aug 1, 2026 by crei Collaborator • Draft
7
ProTip! Updated in the last three days: updated:>2026-08-14.