We're posting lots of papers written with GPT-6 Astra on generalization properties of bayesian neural net learning. [1] The following picture emerges:

GPT-6 Astra has produced Lean formalizations corresponding to each of the 5 papers individually referenced above. [6] The folder contains 30+ more manuscripts which have not been formalized yet [7] ; our guess is that each manuscript is correct [8] .

If you want to understand this research program, we recommend starting from these slides to understand the setup and some key ideas, and then reading the FAQ to get a sense of the current state of the agenda, including its many open problems.

specifically, the "mean field" prior and priors which are "stronger" than it; you can think of these as priors that care a bunch about minimizing norm ↩︎

except for exponentially small probability in the choice of , and this assumes no distribution shift between train and test ↩︎

There is a host of possible conditions here; there are open research directions of understanding how reasonable our candidate conditions are, coming up with more natural alternative conditions, or arguing that there isn't any very natural condition. For some cases, it is open if a robustness assumption is needed at all. ↩︎

specifically, certain priors that care about norm less than the mean field prior ↩︎

Opus 5.5 reviewed these formalizations and said all theorem statements were formalized correctly. ↩︎

because we didn't want to throw more money into tokens at this time ↩︎

possibly modulo minor errors that don't kill the result or the proof strategy, as usual in math ↩︎