ROOM: Auditorium CIC/EST

Euclid's lemma is a simple, yet fundamental result and tool in elementary number theory. In the English Wikipedia it is stated as: If a prime $p$ divides the product $ab$ of two integers $a$ and $b$, then $p$ must divide at least one of those integers $a$ or $b$.

For our formalization of perfectoid rings in the natural language proof checker Naproche we needed a proof of the lemma which only employs non-negative integers. In the Wikipedia article we found such a proof, which we translated by hand, staying close to the original language and proof structure.

In our talk we will present the proof and use it to demonstrate some Naproche principles. We shall then report how ChatGPT was able to produce a similar proof automatically from the Wikipedia text after being tought sufficiently many Naproche principles in an interactive "conversation".

This work presents a formalization of the ideology Social Darwinism using Naproche, a controlled natural language proof-checking system. The ideology is translated into a precise mathematical model, with assumptions made explicit and conclusions derived unambiguously. The study demonstrates how formalization, a practice common in economic theory and mathematics, can enhance transparency, verifiability, and reproducibility in the analysis of conceptual systems.

Naproche combines natural mathematical language with automated reason-ing. Definitions, theorems, and proofs are interpreted in first-order logic and checked by automated provers. This preserves the readability of conventional mathematical exposition while enabling formal verification, without requiring extensive prior experience with proof assistants. As a result, it opens formalization to a wider audience beyond mathematicians, including economists and related researchers.

The rationale for formalizing ideologies is that coherent worldviews can, in principle, be expressed in formal terms. Once formalized, they can be analyzed systematically, with assumptions exposed to structured critique and conclusions verified independently of rhetoric or intuition. In this work, such a critique of Social Darwinism is carried out, showing how formalization not only clarifies the logical structure of an ideology but also provides a rigorous framework for its critical evaluation.

Future research may extend this framework to additional ideologies, enabling systematic comparison and advancing a formalized approach to complex sociopolitical thought. The results indicate that formal methods are not confined to mathematics but can be applied more broadly, yielding objective, verifiable models and facilitating critical engagement.

Naproche is a proof assistant that accepts formalizations written in LATEX. This allows the source files of those formalizations on the one hand to be passed to Naproche to be checked for logical correctness (the "logical level") and on the other hand to be passed to a TEX engine to be rendered as, e.g., PDF or HTML (the "presentational level"). However, this poses the challenge that several language a Naproche formalization can make use of must be specified both on the logical and the presentational level. Examples of such language features are:

• referencing formal statements across formalizations;
• reusing symbolic notations across formalizations;
• including formalizations into each other.

Whereas the features listed above are already supported on the logical level of Naproche, they are currently all lacking proper support on the presentational level.

In this talk, we will present how STEX [2] (a LATEX package to create semantically annotated documents) can be integrated into the Naproche ecosystem to provide presentational support for all three language features from the above list.

Moreover, we will demonstrate how FLAMS [1] (a framework for managing semantically annotated documents) can be integrated in the Naproche workflow to manage and facilitate the build process of both PDF and HTML presentations of formalizations – which is also currently lacking proper support in the Naproche ecosystem.

• [1] https://github.com/FlexiFormal/FLAMS
• [2] https://github.com/slatex/stex