Skip to content

feat: Coding Theory, Gilbert Varshamov - #844

Draft
wurtylex wants to merge 1 commit into
leanprover:mainfrom
wurtylex:coding-theory/gilbert-varshamov
Draft

feat: Coding Theory, Gilbert Varshamov #844
wurtylex wants to merge 1 commit into
leanprover:mainfrom
wurtylex:coding-theory/gilbert-varshamov

Conversation

@wurtylex

@wurtylex wurtylex commented Aug 28, 2026

Copy link
Copy Markdown

We ported the majority of the code from https://github.com/wurtylex/LeanECC/tree/main.

We provide a basis for starting coding theory in cslib by providing formalization of

  • Basic code and code properties.
  • Hammingballs.
  • Gilbert Varshamov bounds.

AI Statement

Todo..

Other Todos

  • Follow Doc Header mathlib
  • Follow PR title for commit convention.
  • Take one final cleanup look

@wurtylex wurtylex changed the title ported everything over from leanecc (relevanent to gbv) feat(Coding Theory): Gilbert Varshamov Bounds. Aug 28, 2026
@wurtylex wurtylex changed the title feat(Coding Theory): Gilbert Varshamov Bounds. feat: Coding Theory, Gilbert Varshamov Aug 28, 2026
@ctchou

ctchou commented Aug 28, 2026

Copy link
Copy Markdown
Collaborator

I know this is still a draft, but I have two suggestions:

  • Please add the reference to references.bib and refer to it like in a paper.
  • Please split into 2 or 3 PRs to facilitate digestion by the reviewers.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants