One can possibly make some headway by switching from a traditional formulation of a field of mathematics to a "synthetic" formulation, where the objects under study are not explicitly built out of smaller pieces, but are universally characterized axiomatically. The historical prototype of such an approach is "synthetic differential geometry", where instead of defining what a smooth manifold is in the traditional way (which would take a lot of code), one imposes an axiom that guarantees that all objects/types under study behave like differentiable spaces with smooth functions between them.

Such synthetic formulations of traditional mathematics naturally lend themselves to axiomatization in proof management systems, specifically those based on type theory. Indeed, since intuitionistic type theory is precisely the internal logic of locally cartesian closed categories such as the smooth toposes of synthetic differential geometry, these are by design the systems that formalize synthetically formulated theories.

This gets even more pronounced as one passes from ordinary type theory to homotopy type theory, since here basic axioms are already so much more expressive. For instance where in ordinary type theory one formulates group theory in the traditional "piecewise" form, in homotopy type theory one finds that group theory is already built in, right out of the box: in an $\infty$-topos $\mathbf{H}$ group objects are equivalent to pointed connected objects $\mathbf{B}G$, and the slice $\infty$-topos $Act(G) \simeq \mathbf{H}_{/\mathbf{B}G}$ over such is the $\infty$-category of infinity-group actions. In thomotopy type theory this means that a dependent type over a pointed connected type $\mathbf{B}G$ is a group representation (even an $\infty$-group representation up to coherent homotopy), dependent sum now is forming the induced representation, dependent product the co-induced representation. This yields a synthetic formulation of group theory and representation theory in homotopy type theory without adding a single extra axiom.

This option hasn't been explored much yet, as far as I can see, for doing formalized proofs. But I think it would be possible and worthwhile to do so.

One is therefore naturally led to wonder if one can usefully combine the synthetic description of differential geometry and that of higher gauge theory, aka higher group representation theory to find a synthetic formulation of modern higher differential geometry, that would naturally express modern concepts such as differential cohomology, D-module theory, étale stacks and the like. I have been exploring this a little under the name differential cohesive homotopy type theory where all this naturally exists, synthetically. Myself, I am not coding computer managed proofs myself, but for many of the statements that one proves in differential cohesive infinity-toposes it is or would be fairly straightforward to do so. Once on the n-Category Café we went through some basic exercises in this context and for instance proved in Coq from the axioms the long exact sequences that characterize differential cohomology, see here.

For more details, with Mike Shulman we have written an introduction to the synthetic axiomatization of higher differential geometry and higher gauge theory in homotopy type theory:

• Urs Schreiber, Mike Shulman, Quantum gauge field theory in cohesive homotopy type theory

Two weeks ago at the meeting of the Canadian Mathematical Society I advertized this approach further, see

• Urs Schreiber, Synthetic Quantum Field Theory

One can possibly make some headway by switching from a traditional formulation of a field of mathematics to a "synthetic" formulation, where the objects under study are not explicitly built out of smaller pieces, but are universally characterized axiomatically. The historical prototype of such an approach is "synthetic differential geometry", where instead of defining what a smooth manifold is in the traditional way (which would take a lot of code), one imposes an axiom that guarantees that all objects/types under study behave like differentiable spaces with smooth functions between them.

Such synthetic formulations of traditional mathematics naturally lend themselves to axiomatization in proof management systems, specifically those based on type theory. Indeed, since intuitionistic type theory is precisely the internal logic of locally cartesian closed categories such as the smooth toposes of synthetic differential geometry, these are by design the systems that formalize synthetically formulated theories.

This gets even more pronounced as one passes from ordinary type theory to homotopy type theory, since here basic axioms are already so much more expressive. For instance where in ordinary type theory one formulates group theory in the traditional "piecewise" form, in homotopy type theory one finds that group theory is already built in, right out of the box: in an $\infty$-topos $\mathbf{H}$ group objects are equivalent to pointed connected objects $\mathbf{B}G$, and the slice $\infty$-topos $Act(G) \simeq \mathbf{H}_{/\mathbf{B}G}$ over such is the $\infty$-category of infinity-group actions. In homotopy type theory this means that a dependent type over a pointed connected type $\mathbf{B}G$ is a group representation (even an $\infty$-group representation up to coherent homotopy), dependent sum now is forming the induced representation, dependent product the co-induced representation. This yields a synthetic formulation of group theory and representation theory in homotopy type theory without adding a single extra axiom.

This option hasn't been explored much yet, as far as I can see, for doing formalized proofs. But I think it would be possible and worthwhile to do so.

One is therefore naturally led to wonder if one can usefully combine the synthetic description of differential geometry and that of higher gauge theory, aka higher group representation theory to find a synthetic formulation of modern higher differential geometry, that would naturally express modern concepts such as differential cohomology, D-module theory, étale stacks and the like. I have been exploring this a little under the name differential cohesive homotopy type theory where all this naturally exists, synthetically. Myself, I am not coding computer managed proofs myself, but for many of the statements that one proves in differential cohesive infinity-toposes it is or would be fairly straightforward to do so. Once on the n-Category Café we went through some basic exercises in this context and for instance proved in Coq from the axioms the long exact sequences that characterize differential cohomology, see here.

For more details, with Mike Shulman we have written an introduction to the synthetic axiomatization of higher differential geometry and higher gauge theory in homotopy type theory:

• Urs Schreiber, Mike Shulman, Quantum gauge field theory in cohesive homotopy type theory

Two weeks ago at the meeting of the Canadian Mathematical Society I advertized this approach further, see

• Urs Schreiber, Synthetic Quantum Field Theory