Abstract
The rise of cloud-based deep learning sharpens a fundamental question: can useful computation be performed when both the user’s data and the model itself must remain private? I will present quantum-secure multiparty deep learning: an optical processor that performs deep-learning computations directly in weak pulses of light, with security guaranteed by quantum physics rather than computational hardness assumptions [1]. This work motivated a broader move from hand-checked proofs to machine verified reasoning. I will describe our workflow, in which large language models propose mathematical arguments and Lean, a formal proof assistant, checks every logical step [2]. We used this approach to settle the decade-old Farhi, Goldstone, and Gutmann QAOA conjecture [3], and are now applying it to quantum cryptography [4]. The goal is AI-assisted discovery whose results are formally verified. References: [1] Sulimany, Vadlamani, Hamerly, Iyengar, and Englund, “Quantum-secure multiparty deep learning,” Physical Review X 15.4 (2025), arXiv:2408.05629. [2] Breen et al., “Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics,” arXiv:2510.12787 (2025). [3] Kol, Ben-Shahar, Sulimany, and Englund, “A Machine-Verified Proof of a Quantum-Optimization Conjecture,” arXiv:2606.29687 (2026). [4] Ben-Shahar, Morag, Englund, and Sulimany, “Machine-Verified Quantum Cryptography,” in preparation (2026).
