Skip to content

Pull requests: leanprover/cslib

New pull request New
128 Open 629 Closed
128 Open 629 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

feat(Crypto): define PRGs and their security definition
#876 opened Sep 5, 2026 by SamuelSchlesinger Collaborator Loading…
feat(MultiTapeTM): prove resource bounds for function composition
#875 opened Sep 5, 2026 by SamuelSchlesinger Collaborator Loading…
feat(MultiTapeTM): compose machines using tape transformations
#874 opened Sep 5, 2026 by SamuelSchlesinger Collaborator Loading…
feat(MultiTapeTM): add input and work tape rewinding
#873 opened Sep 5, 2026 by SamuelSchlesinger Collaborator Loading…
feat(MultiTapeTM): redirect input and output through work tapes
#872 opened Sep 5, 2026 by SamuelSchlesinger Collaborator Loading…
feat(MultiTapeTM): add sequential composition and tape extension
#871 opened Sep 5, 2026 by SamuelSchlesinger Collaborator Loading…
refactor(MultiTapeTM): define function complexity on inputs
#870 opened Sep 5, 2026 by SamuelSchlesinger Collaborator Loading…
refactor: define Commute via DiamondCommute
#868 opened Sep 5, 2026 by lengyijun Contributor Loading…
1
chore: bump mathlib to 950d270, fix breaking changes dependency-incompatibility-fix Fix PR for a dependency incompatibility, opened by downstream-reports
#867 opened Sep 4, 2026 by mathlib-nightly-testing Bot Loading…
1
feat(Algorithms/CCS): Diffie-Hellman protocol in Stateful Processes
#865 opened Sep 4, 2026 by fmontesi Collaborator Loading…
@XYUnknown
feat(maintenance): clarifications on decision making and reviewer/maintainer teams
#864 opened Sep 4, 2026 by fmontesi Collaborator Loading…
@arademaker @chenson2018
18
feat(Logic): General Modal Logic logic
#863 opened Sep 4, 2026 by fmontesi Collaborator Loading…
@XYUnknown @thomaskwaring
2
feat(LocallyNameless): FullBetaEta, Normal.sup_iff
#862 opened Sep 4, 2026 by lengyijun Contributor Loading…
feat: add monad-polymorphic sorts
#861 opened Sep 3, 2026 by eric-wieser Collaborator Loading…
feat: sn_eta_steps_inv
#860 opened Sep 3, 2026 by lengyijun Contributor Loading…
refactor: SN adjacent to Terminating
#859 opened Sep 3, 2026 by lengyijun Contributor Loading…
3
feat(MachineLearning/PACLearning): realizable distribution family
#858 opened Sep 3, 2026 by LibertasSpZ Loading…
feat: add a predicate for monad morphisms
#856 opened Sep 2, 2026 by eric-wieser Collaborator Loading…
@sorrachai
chore(Foundations/Relation/Confluence): cleanup
#855 opened Sep 2, 2026 by thomaskwaring Collaborator Loading…
15
feat(MultiTapeTM): Any function constant with finitely many exceptions is computable in constant time and space
#854 opened Sep 2, 2026 by crei Collaborator Loading…
2
refactor(locallynameless): remove HasFresh
#852 opened Sep 2, 2026 by lengyijun Contributor Loading…
refactor(Computability): remove h_mono from PolyTimeComputable.comp
#845 opened Aug 28, 2026 by BoltonBailey Contributor Loading…
1
1
feat: Coding Theory, Gilbert Varshamov
#844 opened Aug 28, 2026 by wurtylex • Draft
1
feat(Computability): add generic circuit model
#841 opened Aug 27, 2026 by SamuelSchlesinger Collaborator Loading…
26
feat(Automata): Two-way automaton
#834 opened Aug 24, 2026 by crei Collaborator Loading…
21
ProTip! Updated in the last three days: updated:>2026-09-02.