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. |

- VECTSP12,
*{I}somorphism Theorem on Vector Spaces over a Ring*, Yuichi Futa and Yasunari Shidama, - DUALSP05,
*{F}. {R}iesz Theorem*, Keiko Narita, Kazuhisa Nakasho and Yasunari Shidama, - RING_5,
*{O}n Roots of Polynomials and Algebraically Closed Fields*, Christoph Schwarzweller, - PELLS_EQ,
*{T}he {P}ell's Equation*, Marcin Acewicz and Karol P\k{a}k, - NOMIN_1,
*{S}imple named-complex valued nominative data -- definition and basic operations*, Ievgen Ivanov, Mykola Nikitchenko, Andrii Kryvolap and Artur Korni{\l}owicz, - COUSIN2,
*{G}auge Integral*, Roland Coghetto, - MESFUN11,
*{I}ntegral of Non Positive Functions*, Noboru Endou, - FUZIMPL1,
*{F}ormal Introduction to Fuzzy Implications*, Adam Grabowski.