All pull requests

Pull requests

• refactor(Circuit): generalize FanIn input support bounds to weighted gate costs (#884)

  #929·SamuelSchlesinger opened Oct 25, 2026Collaborator·

  ·

• feat(FineGrained): the satisfiability coding lemma and PPZ for unique k-SAT (#894)

  #928·SamuelSchlesinger opened Oct 25, 2026Collaborator·

  ·

• feat(Space): NSPACE(s) = coNSPACE(s), with NL = coNL as the case s = log₂ (#885)

  #927·SamuelSchlesinger opened Oct 25, 2026Collaborator·

  ·
  1

• doc(contributing): privatize by intent, not by current usage

  #926·SamuelSchlesinger opened Oct 25, 2026Collaborator·

  ·

• feat(QueryComplexity/Quantum): Grover's algorithm (#896)

  #925·SamuelSchlesinger opened Oct 25, 2026Collaborator·

  ·

• test(PartialMCSP): add nonvacuous instances, verifier runs, and axiom audits (#899)

  #924·SamuelSchlesinger opened Oct 25, 2026Collaborator·

  ·
  1

  1

• feat(QueryComplexity/Quantum): the quantum query model and the BBBV lower bound (#896)

  #923·SamuelSchlesinger opened Oct 25, 2026Collaborator·

  ·

• refactor(Communication): privatize unreferenced declarations in Communication (#899)

  #922·SamuelSchlesinger opened Oct 25, 2026Collaborator·

  ·

• doc(ROADMAP): relocate Luby–Rackoff to classic symmetric constructions (#899)

  #921·SamuelSchlesinger opened Oct 25, 2026Collaborator·

  ·
  1

  1

• feat(NumberTheory/AKS): a modulus of size O(log⁵ n) with large order (#893)

  #920·SamuelSchlesinger opened Oct 25, 2026Collaborator·

  ·

• refactor(Circuit,PH): relocate advice evaluation to Advice and prove PPoly ⊆ PAdvice (#884)

  #919·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·
  1

• feat(abstracts): Immerman–Szelepcsényi headline abstract (#885)

  #918·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·
  1

• feat(NumberTheory/AKS): correctness of the AKS primality tests (#893)

  #917·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·

• chore(tests): build the test library from a Lake glob, removing ComplexityTests.lean

  #916·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·
  3

• feat(LogSpace): 2SAT is NL-complete (#885)

  #915·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·
  1

• feat(NumberTheory/AKS): the AKS identity and the easy direction of correctness (#893)

  #914·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·

• refactor(Crypto/Computational): relocate group surjectivity and add DDH test (#899)

  #910·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·
  3

• feat(FineGrained): Schöning's random walk for k-SAT (#894)

  #908·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·

• feat(Probability/Extractor): two-source extractors and the Chor–Goldreich theorem (#895)

  #905·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·
  8

• refactor(machines): spike, plain closure rules without a tidy calculus (#862)

  #869·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·

• fix(tactic): synthesize plain polytime certificates directly

  #810·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·
  22

• feat(calculus): expose ordinary plain rules from the checked calculus

  #671·SamuelSchlesinger opened Oct 24, 2026Collaborator·

  ·
  4