circuit-complexity

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.

First machine-verified formalization of the natural proofs barrier (Razborov-Rudich 1997) in Lean 4. Zero sorry obligations.

CL-DIAG: Diagnosing canonicalization leakage in supervised learning under group symmetry

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.

Smaller gate-count circuits for GF(2^m) multipliers and the AES S-box, with Lean 4 proofs and verifiers

Código del TFG de Ingeniería Informática / Code for the Computer Science Bacherlor's Thesis

AI-assisted research notebook mapping P vs NP: proof barriers, adversarial falsification, reproducible experiments, formal verification, and a graveyard of failed ideas.