Smaller gate-count circuits for GF(2^m) multipliers and the AES S-box, with Lean 4 proofs and verifiers
-
Updated
Oct 11, 2026 - Lean
Smaller gate-count circuits for GF(2^m) multipliers and the AES S-box, with Lean 4 proofs and verifiers
GF(2) Möbius / zeta transform in o(N log N) XOR gates, the first asymptotic improvement over Yates (1937) for circuits with cancellation: proofs, certificates, Lean 4 checks, and closed ideas. Asymptotic only, AI-checked, not yet human-refereed.
AI-assisted research notebook mapping P vs NP: proof barriers, adversarial falsification, reproducible experiments, formal verification, and a graveyard of failed ideas.
Exact minimal integer-weight threshold circuits for every 4-input Boolean function (65,536 tables, 222 NPN classes): free-weight optima, capped Pareto frontiers, constructive forms, price of decomposability - all machine-verified.
CL-DIAG: Diagnosing canonicalization leakage in supervised learning under group symmetry
First machine-verified formalization of the natural proofs barrier (Razborov-Rudich 1997) in Lean 4. Zero sorry obligations.
Optimal depth for Bell-pair preparation on a 1D chain with fixed local resources, ideal coherent control, and independent noisy measurement reports.
Código del TFG de Ingeniería Informática / Code for the Computer Science Bacherlor's Thesis
To associate your repository with the circuit-complexity topic, visit your repo's landing page and select "manage topics."