Skip to content

Pull requests: leanprover/cslib

New pull request New
103 Open 594 Closed
103 Open 594 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(LTS): convert LTS.Execution from a Prop to a structure
#806 opened Aug 16, 2026 by ctchou Collaborator Loading…
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: Add API of basic constructions
#803 opened Aug 15, 2026 by dtumad Loading…
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
25
refactor(LocallyNameless): Extract depth into a dedicated module
#798 opened Aug 14, 2026 by lengyijun Contributor Loading…
2
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…
8
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 Contributor 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 Contributor 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 Contributor • Draft
7
feat(Crypto): Commitment Schemes
#766 opened Aug 1, 2026 by SamuelSchlesinger Collaborator Loading…
fix: remove grind attr from Xi.step_lc_r
#751 opened Jul 26, 2026 by lengyijun Contributor Loading…
refactor: Add Xi.step_lc_l and simplify step_lc_l in FullBeta/FullEta
#750 opened Jul 26, 2026 by lengyijun Contributor Loading…
refactor: Simplify FullEta.step_lc_r proof
#749 opened Jul 26, 2026 by lengyijun Contributor Loading…
fix(PACLearning): restrict consistency to realizable samples
#747 opened Jul 25, 2026 by SamuelSchlesinger Collaborator Loading…
feat(LambdaCalculus/Named/Untyped): Alpha equivalence equalities
#741 opened Jul 22, 2026 by chris-anto-froeschl Contributor Loading…
@chenson2018
2
ProTip! Adding no:label will show everything without a label.