References
- Aczel, P. “Notes Towards a Formalisation of Constructive Galois Theory,” Technical report, Manchester University, 1994.
- Baanen, A., Dahmen, S. R., Narayanan, A., and Nuccio, F. A. E. 2021. A formalization of Dedekind domains and class groups of global fields.
- Bernard, S., Cohen, C., Mahboubi, A., and Strub, P.-Y. “Unsolvability of the Quintic Formalized in Dependent Type Theory.” Available at: https://hal.inria.fr/hal-03136002, February 2021.
- Buzzard, K., Commelin, J., and Massot, P. 2020. Formalising perfectoid spaces. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs.
- Commelin, J., Lewis, R. Y. 2020. Formalizing the ring of Witt vectors.
- de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J. 2015. The lean theorem prover (system description). In Automated deduction—CADE 25, volume 9195 of Lecture Notes in Comput. Sci., Cham: Springer, pp. 378–388.
- de Vilhena, P. E., Paulson, L. C. 2020. Algebraically closed fields in Isabelle/HOL. In: Peltier, N., Sofronie-Stokkermans, V., eds. Automated Reasoning–10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II, Volume 12167 of Lecture Notes in Computer Science, Cham, Switzerland: Springer; pp. 204–220.
- Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L. 2013. A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D., eds. Interactive Theorem Proving, Berlin, Heidelberg: Springer Berlin Heidelberg; pp. 163–179.
- Han, J. M., van Doorn, F. 2019. A formalization of forcing and the unprovability of the continuum hypothesis. In 10th International Conference on Interactive Theorem Proving, Volume 141 of LIPIcs. Leibniz Int. Proc. Inform., pages Art. No. 19, 19. Wadern: Schloss Dagstuhl. Leibniz-Zent. Inform.
- The mathlib Community. 2020. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020). New York: Association for Computing Machinery, pp. 367–381.
- Milne, J. S. 2020. Fields and Galois theory (v4.61). Available at: www.jmilne.org/math/.
- Schwarzweller, C. 2020. Ring and field adjunctions, algebraic elements and minimal polynomials. Formalized Mathematics, 28: 251–261.