Proving theorems in combinatorics on words using Lean 4.
-
Updated
Mar 24, 2025 - Lean
#
combinatorics-on-words
Here are 11 public repositories matching this topic...
Language: All
Filter by language
Sort: Most stars
Sort options
Souce code for my MSc Thesis in Computer Science "Nested Marvellous Sequences"
de-bruijn-graphs low-discrepancy-sequences de-bruijn-sequence combinatorics-on-words nested-marvellous-sequences marvellous-sequences
-
Updated
Jan 6, 2021 - Haskell
A Haskell module exporting five functions that implement enumeration mechanisms described in Theorem 6.4 from the monograph A.O. Matveev, Symmetric Cycles, Jenny Stanford Publishing, 2023, and illustrated in Example 6.5.
-
Updated
Jan 23, 2026 - Haskell
A formal proof of the Commutation Lemma in Combinatorics on words.
-
Updated
Jul 3, 2026 - Rocq Prover
A Haskell module exporting functions that implement enumeration mechanisms described in Theorems 7.5, 7.7, 7.9 and 7.11 from the monograph A.O. Matveev, Symmetric Cycles, Jenny Stanford Publishing, 2023, and illustrated in Examples 7.6, 7.8, 7.10 and 7.12.
-
Updated
Jan 23, 2026 - Haskell
Binary Smallest Grammar Problem NP-completeness candidate proof - manuscript, verification code, reproducibility tests, and expert-audit materials.
reproducible-research np-complete finite-fields data-compression theoretical-computer-science formal-languages string-algorithms algorithmic-information-theory computational-complexity binary-strings complexity-theory slp grammar-compression lossless-compression combinatorics-on-words assembly-index open-problem research-preprint smallest-grammar-problem straight-line-programs
-
Updated
Sep 3, 2026 - TeX
Lyndon words, Duval factorization, necklace and bracelet enumeration, and De Bruijn sequences in pure Python.
-
Updated
Aug 1, 2026 - Python
A Haskell SmirnovWordsModule.hs module exporting six functions for calculating the numbers of Smirnov words over three-letter and four-letter alphabets. Based on Appendix A of the monograph A.O. Matveev, Symmetric Cycles, Jenny Stanford Publishing, 2023.
-
Updated
Jan 24, 2026 - Haskell
First-order-logic decision procedure for automatic sequences (a Walnut-style prover in Rust): adaptive determinization ladder, guess-and-verify FE construction, Fibonacci/Tribonacci/Pell numeration, resource guard, Python API, web GUI. Benchmarked against Walnut.
rust mathematics formal-methods decision-procedure theorem-prover walnut finite-automata combinatorics-on-words automatic-sequences buchi-arithmetic
-
Updated
Aug 22, 2026 - Rust
Word Structures Lab develops open, reproducible mathematical and computational methods for understanding repetition and structure in words, while making the underlying ideas accessible enough to be explored, verified, challenged, and extended by others.
visualization javascript algorithms computational-mathematics discrete-mathematics knowledge-base formal-languages experimental-mathematics morphisms combinatorics-on-words abelian-squares word-combinatorics
-
Updated
Sep 5, 2026 - JavaScript
AI-assisted mathematical research manuscripts with reproducible materials across combinatorics and words, matrix and coding theory, topology, order and discrete geometry, algebra, matroids, and continuous optimization.
reproducible-research coding-theory combinatorics posets commutative-algebra order-theory finite-geometry polyhedral-combinatorics combinatorics-on-words cyclotomic-polynomials combinatorial-designs ai-assisted-research graph-minors extremal-combinatorics noncommutative-algebra matroid-theory log-concavity computer-assisted-mathematics real-rooted-polynomials abstract-polytopes
-
Updated
Sep 6, 2026 - TeX
Add this topic to your repo
To associate your repository with the combinatorics-on-words topic, visit your repo's landing page and select "manage topics."