Calendar

We introduce the concepts of a symmetry-protected sign problem and symmetry-protected magic, defined by the inability of symmetric finite-depth quantum circuits to transform a state into a nonnegative real wave function and a stabilizer state, respectively. We show that certain symmetry protected topological (SPT) phases have these properties, as a result of their anomalous symmetry action at a boundary. For example, one-dimensional Z2 × Z2 SPT states (e.g. cluster state) have a symmetry-protected sign problem, and two-dimensional Z2 SPT states (e.g. Levin-Gu state) have both a symmetry-protected sign problem and magic. We also comment on the relation of a symmetry-protected sign problem to the computational wire property of one-dimensional SPT states and the greater implications of our results for measurement based quantum computing.

Zoom: https://harvard.zoom.us/j/977347126

Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specialists to be built. This is particularly challenging when applying large Transformer language models to tactic prediction, because the scaling of performance with respect to model size is quickly disrupted in the data-scarce, easily-overfitted regime. We propose PACT (Proof Artifact Co-Training), a general methodology for extracting abundant self-supervised data from kernel-level proof terms for co-training alongside the usual tactic prediction objective. We apply this methodology to Lean, an interactive proof assistant which hosts some of the most sophisticated formalized mathematics to date. We instrument Lean with a neural theorem prover driven by a Transformer language model and show that PACT improves theorem proving success rate on a held-out suite of test theorems from 32\% to 48\%.

Zoom: https://harvard.zoom.us/j/99018808011?pwd=SjRlbWFwVms5YVcwWURVN3R3S2tCUT09

In the talk, I will present an equidistribution result for families of (non-degenerate) subvarieties in a (general) family of abelian varieties. This extends a result of DeMarco and Mavraki for curves in fibered products of elliptic surfaces. Using this result, one can deduce a uniform version of the classical Bogomolov conjecture for curves embedded in their Jacobians, namely that the number of torsion points lying on them is uniformly bounded in the genus of the curve. This has been previously only known in a few select cases by work of David–Philippon and DeMarco–Krieger–Ye. Finally, one can obtain a rather uniform version of the Mordell-Lang conjecture as well by complementing a result of Dimitrov–Gao–Habegger: The number of rational points on a smooth algebraic curve defined over a number field can be bounded solely in terms of its genus and the Mordell-Weil rank of its Jacobian. Again, this was previously known only under additional assumptions (Stoll, Katz–Rabinoff–Zureick-Brown).

Zoom: https://harvard.zoom.us/j/99334398740

Password: The order of the permutation group on 9 elements.

An evil mathematician has kidnapped the Harvard Pilgrim! To win his freedom, a group of undergrads must each find their name in a row of boxes. The odds look dire—but we’ll use some probability theory and combinatorics to find a strategy that dramatically improves our chances. Can you help save our hapless mascot?

Please go to the College Calendar to register.