{'fraction_non_alphanumeric': 0.018518518518518517, 'fraction_numerical': 0.0, 'mean_word_length': 5.113043478260869, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Proof of the Jordan Curve Theorem via the Brouwer Fixed Point Theorem

The aim of the paper is to report on MIZAR codification of the Jordan curve theorem, a theorem chosen as a challenge to be completely verified using formal methods at the time when they started being commonly used. Formalization was done based on proofs taken from the literature, where theorems mentioned in the title of the paper from ”Brouwer’s Fixed Point Theorem and the Jordan Curve Theorem” by David Gauld and ”Algebraic Topology” by Allen Hatcher, respectively. The entire work was done through a strong cooperation between Polish and Japanese universities, especially Białystok University and Shinshu University, Nagano.