In years: 2016-2017, the English version of Formalized Mathematics was financed under agreement 548/P-DUN/2016with the funds from the Polish Minister of Science and Higher Education for the dissemination of science. |

- FIELD_1,
*{O}n Roots of Polynomials over K[X]/p*, Christoph Schwarzweller, - LOPBAN12,
*{I}somorphisms from the Space of Multilinear Operators*, Kazuhisa Nakasho, - LOPBAN13,
*{I}nvertible Operators on Banach Spaces*, Kazuhisa Nakasho, - NDIFF_9,
*{I}mplicit Function Theorem. {P}art {II}*, Kazuhisa Nakasho and Yasunari Shidama, - FIELD_2,
*{O}n Monomorphisms and Subfields*, Christoph Schwarzweller, - ORDINAL7,
*{N}atural Addition of Ordinals*, Sebastian Koch, - GLIB_008,
*{A}bout Supergraphs. {P}art {III}*, Sebastian Koch, - NOMIN_5,
*{P}artial Correctness of a Factorial Algorithm*, Adrian Jaszczak and Artur Korni{\l}owicz, - NOMIN_6,
*{P}artial Correctness of a Power Algorithm*, Adrian Jaszczak, - HILB10_4,
*{D}iophantine Sets. {P}art {II}*, Karol P{\k a}k, - HILB10_5,
*{F}ormalization of the {MRDP} Theorem in the {M}izar System*, Karol P{\k a}k.