Conversation
The interface through which the combinators will use machines: a machine reads words from its work tapes and leaves words on them, never touching the output. Configurations are described by equalities. `listTape` (due to Samuel Schlesinger, leanprover#872 — kept name-identical so the copies dedupe when that lands) turns a word into the tape holding exactly it; `wordsCfg` is the configuration whose tapes hold given words, heads at the start; and the postcondition of `TransformsTapes` is a single configuration equality `runFrom … τ = wordsCfg input none ws' out`, which packages halting, word-holding tapes, the rewound input head and the untouched output in one rewritable equation. Specifications then compose by rewriting rather than by per-tape case analyses. `exists_transformsTapes_nop` — halt in one step, every word unchanged, one visited cell per tape — is the first machine through the interface and the check that the format is inhabited exactly as intended. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Building the first real machine against the interface caught this: a `public def` without `@[expose]` cannot be unfolded by importing modules, so a `TransformsTapes` goal cannot even be `intro`d downstream, and Clear.lean needed a white-box `import all` as a workaround. The specification is exactly the kind of definition its consumers unfold, so it is exposed and the workaround dropped. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Mathlib's naming convention for a constructor of an X from a Y. The name now differs from leanprover#872's `listTape`; the credit note says so. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`seq tm₀ tm₁` behaves like `tm₀` until it would halt and then continues as `tm₁`. The design is due to Samuel Schlesinger (leanprover#872): the state space is the sum, and the halting transition of the first phase is mapped to the initial state of the second, so the handoff costs no step. `transformsTapes_seq` composes two transformations with the bounds adding, and is where the interface's single-equality postcondition pays off: the first machine halts in a full `wordsCfg`, which is on the nose a starting configuration for the second. The proof splits the run at the first machine's minimal halting time (`exists_minimal_halting_time`, new in Deterministic.lean along with `runFrom_eq_of_halt`), mirrors phase one through the left embedding (a bounded induction — the embedding commutes with `step` only while the first machine is live), and phase two through the right embedding, which is a genuine step-semiconjugation, so its run lemma is one application of `runFrom_comm_of_step` from leanprover#878 (cherry-picked; this branch now builds on that PR). Space adds via `spaceUsed_add_le`/`spaceUsed_eq_of_workTapePos`, new in TapeLemmas.lean: space depends only on head positions, which both embeddings preserve. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`TidyComputes`: the machine computes its function and halts in the fully normalised configuration — which is exactly a `wordsCfg`, unifying initial configurations, tidy halting configurations and the endpoints of `TransformsTapes` in one description. Tidiness is what the word-transformer interface needs of a machine before it can be run on redirected tapes: a tidy machine ends where the next one can begin. Groundwork for the normal-form construction, whose phases pass through dirty configurations and therefore chain below the `TransformsTapes` level: `Cfg.withState`, and the raw face of sequential composition — `Sequential.leftCfg`/`rightCfg` with their step and run lemmas made public, plus `Sequential.runFrom_seq`, the run of a composite split at the first machine's first halting time. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`instrument tm mark` runs `tm` unchanged while pairing each work tape with a footprint tape whose head moves in lockstep and marks every blank cell it stands on, leaving nonblank cells — in particular an anchor at cell 0 — alone. A head path is connected, so the marked region is an interval: the footprint restores, next to a tape whose garbage may contain embedded blanks, the scannability that the garbage lacks. This is the run phase of the tidy normal form; the sweep phase will erase each pair by walking the footprint towards the anchor. The relation to `tm` splits in two, and the split carries the proof: * everything except the footprints is a projection — `projCfg` forgets the footprint tapes and commutes with `step` unconditionally, so the instrumented run mirrors the original by `runFrom_comm_of_step`, with no induction; * the footprint contents are a function of the run's history, not of its current configuration, so they get their own run invariant (`workTapes_addNat_instrument`): after `τ` live steps a footprint holds `mark` exactly on the cells its partner's head occupied at an earlier time, on top of what it held initially, which is never overwritten. Head alignment (`workTapePos_addNat_instrument`) rides along. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`exists_markAnchors`: the one-step machine that writes the anchor on every footprint tape — all footprints in the same step, so it costs one step regardless of the tape count. `spaceUsed_instrument`: an instrumented run uses exactly twice the space of the original, because each footprint head visits exactly the cells its partner visits — head alignment turns each visited-set equality into an image congruence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The machine that makes garbage erasable: a tape written by an arbitrary computation may contain blanks inside its garbage, so no scan of the tape itself can find the garbage's extent — but the footprint laid down by `instrument` is contiguous with a distinguished anchor at cell 0, and the sweep erases the pair guided by it, outside-in towards the anchor, consuming the anchor last: goRight over the marks to the right end; sweep left erasing both tapes down to the anchor, which is kept while the garbage under it goes; continue sweeping to the left end; walk right over the now-blank cells — the first mark is the anchor, i.e. cell 0 — erase it and halt. Both heads move in lockstep and home together at 0. Time is linear in the footprint interval (`4 * (r - l).toNat + 8`); the heads never leave the interval widened by one cell, so the sweep's space is the instrumented run's own plus a constant (`2 * (r - l).toNat + 4 + K`). The proof is the Clear pattern scaled to four phases: a generic step lemma against a two-tape configuration descriptor (with an `applyWrite` helper — a `match` in the conclusion would be dependent on the transition hypothesis and block reduction), one trajectory induction per phase, the endpoint chain, and a per-moment shape lemma feeding activity and the space bound. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Cslib.lean gains the Sweep module (mk_all), unused hypotheses of internal phase lemmas are underscore-prefixed, and simp argument lists trimmed per the linter. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The footprint marks cells at pre-move positions, so a head's final cell can be an unmarked fresh extremum. `markCurrent` closes the gap in one blank-guarded step — the instrument's own write rule as a standalone machine — after which the marks cover exactly the visited cells, with the anchor safe under a head that happens to be home. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The rewind machine's time bound is restated in terms of the starting head position (`c.inputPos.val + 2`) rather than the input length — an excursion is bounded by the time that produced it, the input length is not. New: `val_moveInputPos_le`, `inputPos_runFrom_le` (heads stray at most one position per step), and `spaceUsed_le_of_workTapePos_const` (a run that never moves a work head visits one cell per tape). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Every computable function has a tidy machine — one halting in the fully
normalised configuration, `wordsCfg (encIn a) none (fun _ => []) (encOut (f a))`
— at a constant-factor cost in time and space:
tidy tm₀ = markAnchors ; instrument tm₀ ; markCurrent ; rewindInput ;
sweepPair 0 ; … ; sweepPair (k₀ − 1)
This is the theorem that lets the word-transformer interface absorb arbitrary
machines: garbage with embedded blanks cannot be found by scanning, so the run
is instrumented with footprints and the sweeps erase each pair guided by them.
The assembly is a telescope of abstract-configuration lemmas — each phase
composite proved for *any* configuration with the right fields, so the nested
`withState` handoffs never materialise as terms — chained by a bundled raw
composition lemma (`seq_spec`: runs, activity and space of `tm₁.seq tm₂` from
those of the parts, the handoff state being live). The sweeps fold over the
pairs with `exists_sweepChain`; the footprint invariant plus one `markCurrent`
step make each footprint exactly the visited interval `Finset.Icc (L j) (R j)`
of its partner, which is what the sweeps require. The bounds close by counting:
the run costs `t`, the rewind costs the head's excursion (≤ t, not the input
length), the sweeps cost the visited intervals (≤ s each way), and every
product of parameters is dominated by `(k₀+1)²·(bound+1)` with total
coefficient 20.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`outputToTape tm` writes what tm would output onto a fresh last work tape whose head stands at the write frontier — design due to Samuel Schlesinger (leanprover#872). The frontier is the output's length, a function of the configuration, so the redirection is an unconditional step-semiconjugation: the run lemma is one `runFrom_comm_of_step`, and the space cost is exactly the written output (spaceUsed_outputToTape), via the new `length_output_mono`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`inputFromTape tm mark` reads its input from a virtual input work tape instead of the real input tape, which it never touches. Redirecting the input through a work tape is due to Samuel Schlesinger (leanprover#872); there the ambiguity between the two input boundaries — both blank, but the head clamps differently at each — is resolved by a boundary classification in the finite control. Here a flag tape carries a single mark at cell -1, in the spirit of the tidy normal form's footprint anchors, so the left boundary is recognised by reading the flag; the simulated configuration then determines the simulating one and the redirection is an unconditional step-semiconjugation. This commit establishes the machine, the embedding `inCfg`, the projections, and the three facts the semiconjugation rests on: the virtual head reads what the input head reads (`vip_read`), the flag marks exactly the left boundary (`flag_read`), and the clamped move tracks the input head (`clampMove_correct`). The clamp reasoning goes through `val_moveInputPos_eq`, a new `omega`-friendly form of the input head's post-move position as a clamped integer, added to Configuration.lean along with `inputSymbol_eq_none_of_boundary`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`Plumbing/StepLemmas.lean` collects the reductions every explicit-machine proof repeats: * `Action.apply_*` field projections, tagged `@[simp]`, so a step reduces with `simp [step, hq, <machine>]` without naming `Action.apply` or dragging the projection debris through fields the caller ignores; `step_apply_of_state` and the per-field `step_*_of_state` give the same for a single-field rewrite, leaving `tm.tr q _ _` folded until the caller computes it. * `SignType.cast_neg_one`/`cast_zero_int`/`cast_one_int`, tagged `@[simp]`. These, with `Turing.val_moveInputPos_eq` (the omega-native clamped move added earlier), are what let head-position goals over the clamping input head close by `simp only [val_moveInputPos_eq, min_def, max_def, SignType.cast_*]; split_ifs <;> omega` instead of by a hand `SignType` case analysis — the pattern that had cost the most in the redirection machines. `clampMove_correct` is refactored onto them as the first customer, dropping its local cast lemmas. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
simpNF caught that Mathlib's simp already reduces SignType casts to Int and that the Action.apply_workTapes projection's LHS self-simplifies. Dropped my copies and the @[simp] on the match-form projection; clampMove closes with SignType.cast in the simp set directly. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`step_inCfg` / `runFrom_inCfg`: one step (hence one run) of `inputFromTape tm` mirrors one step of `tm` under the embedding `inCfg`. The work tapes split into the original tapes (which the sim carries unchanged, `a.workTapes j` on both sides), the virtual input tape and the flag tape (both written nowhere, their heads moving by the clamped amount). The two head-position boundary cases are exactly `clampMove_correct`, closed by `omega`; everything else is the `Action.apply_*` projections meeting the `inCfg_*` projections. With this, all three of the redirection's ingredients — the machine, the three read/move facts, and the run mirror — are in place, and `inputFromTape` joins `outputToTape` as an unconditional step-semiconjugation. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`Cfg.withOutput` and the commuting run `runFrom_outputToTape_withOutput`: since `outputToTape` never writes the real output tape, its run commutes with replacing that output, so the adapter can be run from a configuration whose real output is already non-empty (as `TransformsTapes` quantifies over). And `initCfg_outputToTape = outCfg (initCfg)`, the start-configuration identity that lets a tidy machine's run be transported through the redirection. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The raw sequential-composition lemma (runs, activity and space of tm₁.seq tm₂ from those of the parts) was private in Tidy.lean; the output adapter needs it too, so it moves to Plumbing/Sequential.lean, generalised from Bool to an arbitrary symbol alphabet. Tidy.lean uses the public version. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The output adapter's space bound needs that rewindTape moves the tape-i head only within [-1, w.length] — without it, spaceUsed_linear gives a lossy K*w.length product outside the c*(...)+k bound shape. `runFrom_pos_range` proves the head stays in that interval at every step, and the clause is threaded into `exists_rewindTape`'s per-step conclusion. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`spaceUsed_le_of_one_moving`: if one head stays within an interval and every other head is fixed, the space is the interval plus one cell per other tape — the sharp bound the output adapter needs for the rewind phase (rather than the lossy K*t of spaceUsed_linear). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
An earlier commit titled the same claimed these but a failed assertion had left them unwritten (only an import landed). This adds the real content: Cfg.withOutput, step_/runFrom_/spaceUsed_outputToTape_withOutput (the run and space commute with replacing the real output, since outputToTape never writes it), and initCfg_outputToTape = outCfg (initCfg). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… a tape transformer `exists_transformsTapes_ofComputableInput`: every computable function has a machine that, started with the input on the real input tape and every work tape blank, halts having written the encoded result to the last work tape in the `wordsCfg` normal form — in linear time and space linear in the result length. This is the first bridge from a computable function into the word-transformer interface, and the payoff of the whole machine layer: it is pure assembly of `exists_tidy` (make the function halt tidily), `outputToTape` (redirect the output to a fresh tape), and `rewindTape` (bring that tape's head home), composed by `seq_spec`. The proof is sectioned by phase; the time bound uses that the encoded result is produced by the original machine in ≤ t steps (so it is that short), and the space bound uses the sharp one-moving-head lemma for the rewind phase. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… cell Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The step where we inject `TEST_ARGS` into the `GITHUB_ENV` environment variable was a workaround for a bug in `lean-action`, in which it ignored its own `test-args` input. That fix landed in leanprover/lean-action#153 and is included in `lean-action` since v1.6.0, which is what we pick up here on the CSLib side.
…orms-tapes PR Bring the interface files on this campaign branch in line with the finalized `transforms-tapes` PR (the first split-out PR against main), so that once it lands the campaign PR shows only the remaining work: * `Plumbing/TransformsTapes.lean`, `TapeLemmas.lean`: take the PR's versions verbatim (docstring/normal-form rewrite, section-style visibility, leanprover#768's space lemmas restored). * `Configuration.lean`: `Cfg.withState` moves here from `TransformsTapes`. * `Plumbing/Sequential.lean`: same docstring/section-style cleanup; `seq_spec` and its helpers stay, since they ship with a later PR (Adapters/Tidy use them). Full `lake build --wfail` + `lake lint` + `lint-style` clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Campaign bookkeeping for the tape-transformer / loop work: the intra-module dependency DAG, new-vs-modified file inventory, and the proposed sequence of independently reviewable PRs against main (PR 1 = transforms-tapes finalized), with the foundation-lemma / seq_spec / withState placement decisions recorded. Not part of any split PR; must not be merged into main. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ver#747) Fixes the definition of consistency to have realizability as a precondition.
Add Xueying Qin as reviewer.
We show that various list operations are preserved under monad morphisms, and that FreeM.liftM is. Note that [PolyFun already has the _bundled_ version](https://github.com/Verified-zkEVM/PolyFun/blob/main/PolyFun/Control/Monad/Hom.lean), but having the unbundled version now does not preclude adding the bundled version later. --------- Co-authored-by: Fabrizio Montesi <fm@fabriziomontesi.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
…ence to commutation (leanprover#880) This PR generalises many results from confluent to commuting relations, and obtains the classical case as a specialisation. We add `HJoin` and `MHJoin` — heterogenous versions of `Join` and `MJoin` — and associated API for them and related relational constructions. NB: the theorem `confluent_equivalents` is now public, and the `TFAE` has been extended with certain other properties which generalise better to the heterogenous case. --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au>
Adds notation for CCS processes and updates the vending machine example to use it.
Bump `mathlib` dependency to [87befc8](leanprover-community/mathlib4@87befc8): doc(DerivNotation): remove stale "future work" note (#43662) (2026-09-13) Previously at: [950d270](leanprover-community/mathlib4@950d270): feat(TacticAnalysis): suggest `rwa` for `rw` followed by `assumption` (#42732) (2026-09-04) --- This is an automated dependency bump to the latest commit this project is known to build against (its **last-known-good** commit). `lake build` was run against the new commit before this PR was opened and succeeded, so it should be mergeable as-is. Only `lake build` is checked, though — if your own CI does more (linting, failing on warnings, downstream tests, …), run it on this PR before merging. _This PR was last updated on 2026-09-13 by [this workflow run](https://github.com/leanprover/cslib/actions/runs/34779898369). It is an automated bump using [downstream-reports/open-bump-pr](https://github.com/leanprover-community/downstream-reports)._ Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
…configurations reachable in bounded space (leanprover#772) Proves an upper bound on the number of configurations reachable in bounded space on a multi-tape TM. The proof introduces the concept of `Storage`, the projection of `Cfg` that only contain the state and the work tapes. It shows that if the TM uses at most `s` space, there is an injection to a structure that only uses `[-s, s]` to index the tape. --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>
…s is computable in constant time and space (leanprover#854) This is a starting point of a Turing machine combinator library, it adds one of the leaves: Any function that is constant with finitely many exceptions is computable in constant time and zero space, relative to any encoding. The same holds for any function with a finite domain. This result captures many functions we want to compose later or with a combinator library: Any function on tuples of `Bool`, for example and "equality comparison with a constant". Together with a "fold" and "composition" combinators, this already allows us to evaluate CNFs or compute `Nat.succ` on binary encoded numbers.
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Fabrizio Montesi <famontesi@gmail.com> Co-authored-by: downstream-lean4[bot] <296232862+downstream-lean4[bot]@users.noreply.github.com> Co-authored-by: downstream-lean4[bot] <downstream-lean4[bot]@users.noreply.github.com>
Add `.github/dependabot.yml` covering the two dependency sources CI actually has. Adding this will enable automatically created PRs if updates (checked weekly) are available, coming from two sources: - GitHub Actions - pip. Look only for minor and patch bumps. (Major versions are excluded, for now.) Related to leanprover#894, which introduces the requirements file the pip entry watches. But mechanically, either one can merge first.
Replace the bare `pip install zulip` calls with a pinned `.github/requirements.txt`. This is pretty small on its own (effectively a no-op), but pinning a version increases reproducibility and helps track issues upstream, should they arise. This also gives Dependabot something to watch, once we've set that up.
Adds a workflow that runs actionlint over the `.github/workflows` directory whenever those files change. actionlint checks expression types (used in the little GitHub Action DSL), undefined step/output references and needs/if conditions, and runs shellcheck over every `run:` shell block and [pyflakes](https://github.com/PyCQA/pyflakes) over `shell: python` chunks. To make sure that adding this workflow does not immediately break the build, I did a manual one-off run and found one thing, which is fixed here: an `echo | sed` pipeline that is now a parameter expansion.
…olating into script text (leanprover#889) Move the key into the step's `env:` block and reference it as a shell variable, matching how the step already receives its other values.
Prove that an element is normal for the supremum of two relations iff it is normal for each of them separately. Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
…leanprover#888) This implements Vardi's construction of a (one-way) finite automaton that accepts the complement of the language accepted by a two-way automaton. Together with closure of regular languages under complement and a simple mapping of one-way automata to two-way automata we get that two-way automata accept exactly the regular languages. AI disclosure: Claude was used throughout bit in a tight review loop.
…on (leanprover#897) Introduce an abstraction over Turing machines that normalizes head positions and uses `List Symbol` for tape contents with a Hoare-style interface. This abstraction will be used by control-flow combinators to be introduced later. Here are the most important definitions and results: * `Plumbing/TransformsTapes.lean`: `tapeOfList` (a tape holding exactly a word), `wordsCfg` (a configuration whose tapes hold given words), `TransformsTapes` (started on word-holding tapes, halt in the normal form `wordsCfg input none ws' out` with the new words related to the old by a postcondition, within given time/space), its `.imp` weakening, and `exists_transformsTapes_nop` as the inhabiting example. * `Plumbing/Sequential.lean`: `transformsTapes_seq`, running one transformer then another. The halting configuration of the first is a valid starting configuration for the second, so the two chain by rewriting with the normal-form equality. * `TapeLemmas.lean`: add the visited-set / space-usage lemmas the interface needs (`visitedByTapeHead_add`, `spaceUsed_add_le`, `spaceUsed_eq_of_workTapePos`, `exists_visitedByTapeHead_eq_Icc`, `spaceUsed_le_of_one_moving`, ...). * `Configuration.lean`: add the state-remap embeddings `Cfg.mapState` and `Cfg.withState`, used to place a sub-machine's configurations into a larger one. * `Deterministic.lean`: add `runFrom_eq_of_halt` and `exists_minimal_halting_time`. AI disclosure: Claude code was heavily used in a tight review loop. --------- Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Add Boolean synthesis with sharing and prove the uniform (1 + ε) 2^n/n upper bound for De Morgan circuits. Assisted by Codex, adapted from https://github.com/samuelSchlesinger/algebraic-circuits.
…ids (leanprover#903) This PR develops yet another characterization of regular languages: a language is regular if and only if its syntactic monoid is finite. The syntactic monoid is the quotient of the free monoid by the Myhill congruence, which is a two-sided congruence on finite words that is finer than the Nerode congruence used in the Myhill-Nerode theorem. As part of this PR, both left and two-sided congruences on finite words are defined and all congruences on finite words are moved from the namespace `Cslib` to the more appropriate namespace `Language`.
Adds Samuel Schlesinger to the area maintainers for complexity, crypto, and learning theory.
Add semantic normalization and counting to prove the worst-case 2^n/n lower bound for De Morgan circuits. Assisted by Codex, adapted from https://github.com/samuelSchlesinger/algebraic-circuits. --------- Co-authored-by: Christian Reitwiessner <crei.github@gmail.com>
Allows Samuel Schlesinger to accept PRs. (I had previously forgotten to do this in the PR adding him as maintainer.)
I (@chenson2018) have intervened manually here because of the cache issue, manually doing a `lake update` (and making the one line Mathlib adaptation). Closes leanprover#933 --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
9 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.