ABSTRACT. Many problems for formal verification and artificial intelligence rely on advanced reasoning technologies in the background, often in the form of SAT or QBF solvers. Such solvers are sophisticated and highly tuned pieces of software, often too complex to be verified themselves. Now the question arises how one can one be sure that the result of such a solver is correct, especially when its result is critical for proving the correctness of another system. If a SAT solver, a tool for deciding a propositional formula, returns satisfiable, then it also returns a model which is easy to check. If the answer is unsatisfiable, the situation is more complicated. And so it is for true and false quantified Boolean formulas (QBFs), which extend propositional logic by quantifiers over the Boolean variables. To increase the trust in a solving result, modern solvers are expected to produce certificates that can independently and efficiently be checked. In this paper, we give an overview of the state of the art on validating the results of SAT and QBF solvers based on certification.

ABSTRACT. Many algorithms in computer algebra and beyond produce answers. For some of these, we have formal proofs of the correctness of the algorithm, and for others it is easy to verify that the answer is correct. Other algorithms produce either an answer or a proof that no such answer exists. It may still be easy to verify that the answer is correct, but what about the ``no such answer'' case. The claim of this paper is that, at least in some cases, it is possible for the algorithm to produce ``hints'' such that a theorem prover can prove that, in this case, there is no such answer.

ABSTRACT. We present a system for the visualization of proofs originating from Automated Theorem Provers for first-order logic. The system can hide uninteresting proof parts of proofs, such as type annotations, translate first-order terms to standard math syntax, and compactly display complex formulas. We demonstrate the system on several non-trivial automated proofs of statements from Mizar Mathematical Library translated to first-order logic, and we provide a web interface where curious users can browse and investigate the proofs.

ABSTRACT. Solving a sparse linear system of the form Ax=b is a common engineering task, e.g., as a step in approximating solutions of differential equations. Inverting a large matrix A is often too expensive, and instead engineers rely on iterative methods, which progressively approximate the solution x of the linear system in several iterations, where each iteration is a much less expensive (sparse) matrix-vector multiplication.

We present a formal proof in the Coq proof assistant of the correctness, accuracy and convergence of one prominent iterative method, the Jacobi iteration. The accuracy and convergence properties of Jacobi iteration are well-studied, but most past analyses were performed in real arithmetic; instead, we study those properties, and formally prove our results, in floating-point arithmetic. We also formally prove that our results are properly reflected in a concrete implementation in the C programming language. Finally, we formally prove that the iteration will not overflow, under assumptions that we make explicit. Notably, our proofs are faithful to the details of the implementation, including C program semantics and floating-point arithmetic.

ABSTRACT. Operations research deals with modeling and solving real-world problems as mathematical optimization problems. While solving mathematical systems is accomplished by analytical software, formulating a problem as a set of mathematical operations has been typically done manually by domain experts. Recent machine learning methods have shown promise in converting textual problem descriptions to corresponding mathematical formulations. This paper presents an approach that converts linear programming word problems into mathematical formulations. We leverage the named entities in the input and augment the input to highlight these entities. Our approach achieves the highest accuracy among all submissions to the NL4Opt Competition, securing first place in the generation track.

ABSTRACT. In this paper, we explore whether a data structure for representing Boolean functions (namely, Binary Decision Diagrams) can be useful to detect, in an efficient way, the acyclicity of simplicial complexes. This is approached by means of the concept of evasiveness, allowing us to study the relation with Alexander duality. Furthermore, as main result, we proved that the (depth) complexity of a kind of acyclic simplicial complexes (dismantlable complexes) can be determined by means of Reduced Ordered Binary Decision Diagrams. As the subject has shown itself error prone, we have carried out the proof by using the Isabelle proof assistant, providing a rewarding combination of informal and formal mathematics.

ABSTRACT. Despite its critical role, remote attestation in Intel Software Guard Extensions (SGX) and Trust Domain Extensions (TDX) is not only underspecified by Intel but also contains various contradictions that could potentially lead to design and implementation flaws. We take the challenge of formal specification and verification of remote attestation mechanism in Intel SGX and TDX. Our most recent work formally demonstrates attacks on Intel's claimed trusted computing base (TCB) for TDX.

ABSTRACT. Let Q(α1, · · ·, αn) be an algebraic number field. We designed a modular gcd algorithm, MGCD, for computing the monic gcd, g, of two polynomials f1, f2 belonging to Q(α1, . . . , αn)[x1, . . . , xk]. To improve the efficiency of MGCD, we use linear algebra to find an isomorphism between Q(α1, . . . , αn) and Q(γ), where γ is a primitive element of Q(α1, . . . , αn). To prevent expression swell, this conversion is performed modulo a prime. Next, we use a sequence of evaluation points to convert the multivariate polynomials to univariate polynomials, enabling us to employ the monic Euclidean algorithm. We currently use dense interpolation to recover x2, . . . , xk in the gcd. In order to reconstruct the rational coefficients in g, we apply the Chinese remaindering(CRT) and the rational number reconstruction(RNR). We have implemented our algorithm in Maple using a recursive dense representation for polynomials.

ABSTRACT. The language of mathematics contains many ambiguities, which make the meaning of mathematical documents more difficult to infer. We hope to make mathematical documents prepared with LaTeX less ambiguous, by producing semantic markup for the mathematical formulas they contain. We will do this using sTeX, a LaTeX macro package for semantic markup, and the accompanying Semantic Multilingual Glossary of Mathematics (SMGloM). The current approach we are investigating is turning collections of semantic macros into context-free grammars to parse formulas and try to infer their structure.

ABSTRACT. How can it be ensured that a robot will move where it is expected to move, and interact with its environment in the way it is expected? This is the fundamental question motivating and underpinning this work. Often this is answered with a simulation of a robotic system. But how would one verify the system using other techniques (such as testing or proof) to confirm the behaviour observed in simulation? This requires using the equations of the model of the robotic system and their solutions, adopted for simulation, and then ensuring that there is consistency with the equations used in testing and proof techniques.

Physics engines are components of a simulator that embody, determine, or use equations describing physical properties or behaviour. They are found across many disciplines, including animated films, video games, and robotics. Physics engines today are often designed to be broad enough to cover multiple domains, rather than focusing on robotic systems alone. For instance, most physics engines favour speed over accuracy when calculating the dynamics of a robotic system. In the context of robotics, this is not ideal, as it exacerbates the reality gap that occurs when behaviour observed in simulation is not reproduced in the real world. There are currently no convenient means by which the developer of a simulation can determine or even find out the underlying equations used by the physics engine. Without this possibility or knowledge, consistency between simulation and other verification techniques cannot be guaranteed.

Besides simulation, verification of a robotic system can involve testing and proof (using model checkers and theorem provers such as FDR and Isabelle). Testing and simulation alone are not enough for the verification of safety-critical or mission-critical robotic systems. With complementary proof-based verification, one can ensure that observations in testing and simulation apply for all scenarios. Use of a variety of verification techniques, however, is only effective if any observations in simulation can be expected to be consistent with the proof of any properties relating to the robot and the environment. This is only possible if one can guarantee that the simulation and the proof use the same models, and that the error due to the solution of any behavioral equations of these models used in simulation is accounted for. Ensuring consistency between simulation and proof reduces the amount of testing required in the verification of a robotic system, thereby reducing costs. Examples where proof has been considered as part of the verification of a robotic system include surgical robots and robotic ground vehicles.

Consistency is defined as follows.

Consistency: "A simulation and a proof of a property of a robotic system are consistent if the equations used in the mathematical model adopted in the proof are the same as those used in simulation."

The following research hypothesis summarises the goal of the thesis.

Research Hypothesis: "It is possible to provide techniques and tools for use of a physics engine in a simulation that can be used in the verification of robotic systems under full consistency with proof."

We aim to complete the current work which aims to partially tackle the above research hypothesis by the end of July in time for submission to ICRA. In particular, our contributions here are threefold. First, we describe a simulation framework, including each of its artefacts and techniques. Second, we provide a manual implementation of the code generation steps of our framework. We show that we can achieve transparency up to high-level functions involved in forward dynamics computations and at a very high cost. Finally, we demonstrate how our choice of simulator, Drake, and our choice of modelling language, RoboSim, can be adapted to use our framework, and the limitations of this approach with respect to consistency.

In our framework, intermediary representations of behavioural equations and their solution bridge the gap between behavioural equations of components at the model level, and the animation of a robotic system by a physics engine. Physics engines currently make use of SDF to describe aspects of the model of a robotic system, however, our intermediary representations extend SDF to include OpenMath, which allows us to include information relating to behavioural equations and their solution. We look to obtain feedback on this aspect of our work at the CICM doctoral symposium.

The rules describing the automatic generation from model, to intermediary representations and their solution, to code which can be used by a physics engine, is to be undertaken until January 2024. Following this we aim to submit this portion of our work to a computer science conference or journal.

In parallel with this work, we aim to carry out further case studies through which properties about kinematic singularities are proven, which are also observed in simulation. We aim to publish these results in a suitable robotics journal or conference.

ABSTRACT. In my PhD thesis I propose to explore the capabilities of using theory morphisms to improve adaptive learning systems. Thereby I aim to adresses the problem of handling interrelations between mathematical theories in automated processes for managing education material.

ABSTRACT. The ALeA system (Adaptive Learning Assistant) offers learners highly interactive learning materials, leveraging a fine-grained domain model, learner profiling, and semantically annotated learning objects, to create personalized course content.

This paper focuses on ALeA’s user interface, through which learners interact with active documents. We outline the representation scheme of these documents and elucidate their features designed to enhance the learning experience. Moreover, we delve into the abstractions and complexities addressed by the client-side React (javascript) library to enable these features.

ABSTRACT. The ALeA system (Adaptive Learning Assistant) uses a fine-grained domain model, a learner model based on it, and semantically annotated learning objects to generate user-adaptive and interactive course materials for pre-/post-paration of lectures and self-study. In this paper we propose new interactions and learning support services that enhance the learner experience without requiring new markup facilities – in essence enhancing the didactic capabilities of the system without further investment into marking up learning objects.

ABSTRACT. In this study, we analyze computer-aided inquiry-based mathematics learning and illustrate how the learning constructs are represented in the learning data. A Moodle plug-in associated with the dynamic geometry software CindyJS was used to record fine-grained log data of learners' manipulations of the dynamic content on the web. Our previous study indicates that some characteristic quantity calculated from the log data can serve as an indicator of the occurrence of some productive failure in learners' inquiry and teacher intervention can prompt those failures. However, the relationship between the occurrence of those failures and the learning constructs created through the whole manipulation process has not been fully investigated. In this study, we examine the temporal change of the characteristic quantity across those failures and consider how the learning constructs are represented in the log data of manipulations.

ABSTRACT. This paper describes an experimental framework for creating an E-Learning system. This framework is designed to be used by teachers in schools, and by utilizing HTML5 technology, can create an E-Learning system on PCs without the need for a special server. The E-Learning system created is a web application consisting of a single HTML file, which can be used not only on a PC, but also on tablets and smartphones.

The E-Learning system created from this framework is characterized by its dual-layered screen structure. By placing existing educational materials and websites on the lower layer of the two-tier structure and adding additional textboxes and buttons on the upper layer, it is possible to convert existing educational materials and websites into an E-Learning system.

In addition, various functions can be added to the system by utilizing JavaScript libraries. For example, by incorporating Algebrite, a JavaScript library for symbolic computation, it is possible to perform symbolic computation of mathematical expressions, which can then be used to automatically grade students' answers.

In this paper, after outlining the structure of this framework, the JavaScript library used will be described. After that, the flow of actually constructing an E-Learning system using this framework will be explained step by step.

ABSTRACT. The language of mathematical texts, e.g., descriptions, definitions, statements, and proofs, is typically a specialised natural language, suitably interleaved with mathematical symbols and expressions. Fragments of mathematical language are carefully written, e.g., by:

(1) using grammatically well-formed expressions, with respect to major syntactic categories of natural language, of lexemes, phrases, sentences

(2) targeting unambiguous expressions, by eliminating or minimising ambiguities, which are abundant in natural language.

Such factors demonstrate that computational grammar, including syntax and semantics, is essential for processing of mathematical texts. Among the goals is to provide interconnections with verification and proof systems, and integration with macine learning.

Computational syntax of natural language has been an active area since 1950s, with significant achievements of computational grammars. Computational semantics was introduced by methods of mathematical logic, in 1970s. It continues to be an open, active area of development of specialised formal languages, logic, and type theories. For full adequateness, computational grammar targets covering syntax-semantics interfaces, via parsing natural language for rendering it into formal language. Suitable language of logic can provide rendering of mathematical texts into formal expressions, which can be used in computational interfaces with verification and proof systems, as well as with machine learning.

In the talk, I present compositional interface in computational grammar for rendering natural language of mathematics into terms of the formal language (LAR) of acyclic recursion, by using its type theory, calculi, and syntax-semantics interfaces.

I introduce the technique for a class of expressions involving quantifiers, definite descriptors, and relative clauses, in noun phrases (NPs), which are integrate compounds of mathematical texts. I show the roles of logic operators in sentences and in other phrasal constructs.

I employ Generalised Constraint-Based Lexicalized Grammar (GCBLG) of natural language, which represents major, common syntactic characteristics of a variety of approaches to computational grammar, e.g., Head-Driven Phrase Structure Grammar (HPSG), Lexical Functional Grammar (LFG), Categorial Grammar (CG), and Grammatical Framework (GF).

The LAR terms of mathematical language can surve several major tasks:

(1) LAR provides computational semantics of the language of mathematics, via the syntax-semantics of LAR. LAR has two layers of semantics:

(a) denotational semantics, i.e., den(A), for every LAR term A (b) algorithmic semantics: the calculi of LAR determines the algorithmic process, alg(A), of every meaningful LAR term A, for computing its denotation den(A)

(2) LAR provides facility for representing major semantic ambiguities and underspecification, at the object level of its formal language, without recourse to meta-language variables. Specific semantic representations can be obtained by instantiations of underspecified LAR terms, in context.

(3) LAR terms can provide input into verification and proof systems (open tasks)

(4) the output of verification and proof systems can provide inferences to be rendered back into natural language of mathematical texts (open tasks).

References

[1] Bresnan, J.: Lexical-Functional Syntax. Blackwell Publishers, Oxford (2001)

[2] Buszkowski, W.: Mathematical Linguistics and Proof Theory. In: J. van Benthem, A. ter Meulen (eds.) Handbook of Logic and Language, pp. 683–736. North-Holland, Amsterdam (1997). DOI https://doi.org/ 10.1016/B978-044481714-3/50016-3

[3] DELPH-IN: Deep Linguistic Processing with HPSG (DELPH-IN) (2018, edited). URL http://moin. delph-in.net. Accessed 20-Aug-2023 [

4] Gallin, D.: Intensional and Higher-Order Modal Logic: With Applications to Montague Semantics. North- Holland Publishing Company, Amsterdam and Oxford, and American Elsevier Publishing Company (1975). URL https://doi.org/10.2307/2271880

[5] The Grammatical Framework GF. http://www.grammaticalframework.org. Accessed 20-Aug-2023

[6] Loukanova, R.: Relationships between Specified and Underspecified Quantification by the Theory of Acyclic Recursion. ADCAIJ: Advances in Distributed Computing and Artificial Intelligence Journal 5(4), 19–42 (2016). URL https://doi.org/10.14201/ADCAIJ2016541942

[7] Loukanova, R.: An Approach to Functional Formal Models of Constraint-Based Lexicalized Grammar (CBLG). Fundamenta Informaticae 152(4), 341–372 (2017). DOI 10.3233/FI-2017-1524. URL https: //doi.org/10.3233/FI-2017-1524

[8] Loukanova, R.: Computational Syntax-Semantics Interface with Type-Theory of Acyclic Recursion for Underspecified Semantics. In: R. Osswald, C. Retoré, P. Sutton (eds.) IWCS 2019 Workshop on Computing Semantics with Types, Frames and Related Structures. Proceedings of the Workshop, pp. 37– 48. The Association for Computational Linguistics (ACL), Gothenburg, Sweden (2019). URL https: //www.aclweb.org/anthology/W19-1005

[9] Loukanova, R.: Gamma-Reduction in Type Theory of Acyclic Recursion. Fundamenta Informaticae 170(4), 367–411 (2019). URL https://doi.org/10.3233/FI-2019-1867

[10] Loukanova, R.: Gamma-Star Canonical Forms in the Type-Theory of Acyclic algorithms. In: J. van den Herik, A.P. Rocha (eds.) Agents and Artificial Intelligence, Lecture Notes in Computer Science, vol. 11352, pp. 383–407. Springer International Publishing, Cham (2019). URL https://doi.org/10.1007/ 978-3-030-05453-3_18

[11] Loukanova, R.: Type-Theory of Acyclic Algorithms for Models of Consecutive Binding of Functional Neuro-Receptors. In: A. Grabowski, R. Loukanova, C. Schwarzweller (eds.) AI Aspects in Reasoning, Languages, and Computation, vol. 889, pp. 1–48. Springer International Publishing, Cham (2020). URL https://doi. org/10.1007/978-3-030-41425-2_1 [

12] Loukanova, R.: Algorithmic Dependent-Type Theory of Situated Information and Context Assessments. In: S. Omatu, R. Mehmood, P. Sitek, S. Cicerone, S. Rodr ́ıguez (eds.) Distributed Computing and Artificial Intelligence, 19th International Conference, vol. 583, pp. 31–41. Springer International Publishing, Cham (2023). DOI 10.1007/978-3-031-20859-1 4. URL https://doi.org/10.1007/978-3-031-20859-1_4

[13] Loukanova, R.: Eta-Reduction in Type-Theory of Acyclic Recursion. ADCAIJ: Advances in Distributed Computing and Artificial Intelligence Journal 12(1), 1–22, e29199 (2023). URL https://doi.org/10. 14201/adcaij.29199

[14] Loukanova, R.: Restricted Computations and Parameters in Type-Theory of Acyclic Recursion. ADCAIJ: Advances in Distributed Computing and Artificial Intelligence Journal 12(1), 1–40 (2023). URL https: //doi.org/10.14201/adcaij.29081

[15] Montague, R.: The Proper Treatment of Quantification in Ordinary English. In: J. Hintikka, J. Moravcsik, P. Suppes (eds.) Approaches to Natural Language, vol. 49, pp. 221–242. Synthese Library. Springer, Dordrecht (1973). URL https://doi.org/10.1007/978-94-010-2506-5_10

[16] Moortgat, M.: Categorial Type Logics. In: J. van Benthem, A. ter Meulen (eds.) Handbook of Logic and Language, pp. 93–177. Elsevier, Amsterdam (1997). URL https://doi.org/10.1016/B978-044481714-3/ 50005-9

[17] Moschovakis, Y.N.: The formal language of recursion. Journal of Symbolic Logic 54(4), 1216–1252 (1989). URL https://doi.org/10.1017/S0022481200041086

[18] Moschovakis, Y.N.: Sense and denotation as algorithm and value. In: J. Oikkonen, J. Väänänen (eds.) Logic Colloquium ’90: ASL Summer Meeting in Helsinki, Lecture Notes in Logic, vol. Volume 2, pp. 210– 249. Springer-Verlag, Berlin (1993). URL https://projecteuclid.org/euclid.lnl/1235423715

[19] Moschovakis, Y.N.: The logic of functional recursion. In: M.L. Dalla Chiara, K. Doets, D. Mundici, J. van Benthem (eds.) Logic and Scientific Methods, vol. 259, pp. 179–207. Springer, Dordrecht (1997). URL https://doi.org/10.1007/978-94-017-0487-8_10

[20] Moschovakis, Y.N.: On founding the theory of algorithms. In: H. Dales, G. Oliveri (eds.) Truth in mathematics, pp. 71–104. Clarendon Press, Oxford (1998)

[21] Moschovakis, Y.N.: A Logical Calculus of Meaning and Synonymy. Linguistics and Philosophy 29(1), 27–89 (2006). URL https://doi.org/10.1007/s10988-005-6920-7

[22] Plotkin, G.D.: LCF considered as a programming language. Theoretical Computer Science 5(3), 223–255 (1977). URL https://doi.org/10.1016/0304-3975(77)90044-5

[23] Scott, D.S.: A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science 121(1), 411–440 (1993). URL https://doi.org/10.1016/0304-3975(93)90095-B [24] Thomason, R.H. (ed.): Formal Philosophy: Selected Papers of Richard Montague. Yale University Press, New Haven, Connecticut (1974)

ABSTRACT. The Naproche system (for Natural Proof Checking) [1, 2] interactively proof-checks natural language mathematical texts whilst they are being editing. Input texts are written in the controlled natural language ForTheL (for Formula Theory Language) [3] which is intended to approximate the natural mathematical language. Since ForTheL uses a LaTeX format, high-quality typesetting of formalizations is immediately available. Over the last years a number of theorems from non-trivial university mathematics have been formalized in Naproche. Naproche is distributed as part of the Isabelle prover platform which also includes a selection of Naproche formalizations. Some of these texts closely resemble material that could be found in mathematics textbooks.

Although Naproche allowed to achieve natural mathematical readability for strictly proof-checked formalizations, the formalization process has been slow and arduous. Users not only have to write a logically correct formal document for the intended mathematical content, but at the same time they have to struggle with the weaknesses of ATPs in dealing with implicit proof tasks; they have to observe the rules of LaTeX and ForTheL; and ideally they should aim for natural readability and mathematical elegance of the typeset document. These simultanuous requirements are becoming even more problematic as formalizations are getting longer, sometimes comprizing twenty or more typeset pages, so that the automated background provers are having difficulties to resolve proof tasks within seconds. But this is incompatible with productive interactive work.

In my talk I shall illustrate and analyse the present state of affairs and suggest ways in which natural proof checking could be made usable for a wider mathematical public and for more advanced mathematics. I shall discuss several possible ways forward:

A) Invest massively in improving all components of the current ℕaproche system: e.g., with an editor like TeXmacs [4] users could directly work on typeset mathematics; comprehensive caching of proofs should accelerate proving times by an order of magnitude; tune or train external provers for the specific proof tasks generated by ℕaproche; use standard type-checking routines for some ℕaproche type-checking, etc.

B) Program a new natural system that circumvents weaknesses and complications of ℕaproche; at the moment, Adrian De Lon is working towards a novel set-theory based natural proof assistant.

C) Combine the natural language approach of ℕaproche with established systems. Such a project may have some similarities with the introduction of the Mizar-type proof language Isar in Isabelle/HOL [5].

[1] https://naproche.github.io/index.html

[2] Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Makarius Wenzel: The Isabelle/Naproche Natural Language Proof Assistant. In: Automated Deduction – CADE 28: 28th International Conference on Automated Deduction (Proceedings), 2021, pp. 614–624.

[3] Andrei Paskevich: The syntax and semantics of the ForTheL language. 2007. URL: http://nevidal.org/download/forthel.pdf

[4] http://texmacs.org/tmweb/home/welcome.en.html

[5] https://isabelle.in.tum.de/

ABSTRACT. The Naproche proof assistant checks formalizations written in controlled natural language and fills in gaps in proofs with the help of automated provers such as E and Vampire.

Naproche aims to lower the barriers to entry for mathematicians by modelling natural language and informal proof structures, re-using familiar LaTeX syntax, and emphasizing proof automation. It is possible to formalize nontrivial mathematics in Naproche, and students have successfully completed formalizations covering parts of analysis, linear algebra, representation theory, set theory, category theory, and more. However, the current implementation struggles to scale beyond formalizations that span a few chapters of a textbook. The following are some of the issues we are facing:

Check times. Long formalizations take hours to check. Small inefficiencies, increasingly difficult tasks for automated provers, and lack of parallelism add up to a painful experience even on powerful PCs. Libraries. These general performance issues combined with Naproche’s limited import mechanism (similar to an include directive) makes it difficult to develop more interconnected formalizations or a standard library that other formalizations can build on. Structures. Naproche has no features dedicated to mathematical structures. This means that users have to set up structures themselves. Moreover, dealing with notation becomes cumbersome, such as having to explicitly annotate which structure an operation belongs to. Surface area for user error. It is still too easy for users of Naproche to set themselves up for problems. Some parts of formalizations, such as some top-level functions, have to be formalized using axioms, which can lead to accidental contradictions. The grammar of the controlled language is in parts overly permissive, leading to unintended results. Stability of formalizations. Adding new theorems in the middle of a formalization (or adding imports) adds additional premises to subsequent tasks exported to automated provers. This makes it more difficult for automated provers to find proofs, which then can break existing proofs in Naproche. When flying too close to the resource limits given to automated provers, formalizations become flaky or fail to be reproducible on other computers. To address the issues described above, I’m working on a new implementation of Naproche. The new proof assistant is developed in tandem with a more inter- connected and modular “standard library” of mostly undergraduate material, which shall serve as a foundation for future formalizations. Using parallelism and premise selection the new proof assistant is currently roughly ten times faster.

In my talk I will present my current progress and discuss the development of the new proof assistant and its standard library. I will talk about how some of the issues described above are mitigated in the new implementation. I will also talk about the following:

Initial user impressions. How does the formalization process compare to the previous implementation? Are there any compromises? Library design. Formalizing a standard library both with readability for humans and granularity for automated proofs in mind. Premise selection. Arguably the biggest contributor to long checking times are increasingly difficult tasks for automated provers. Using premise selection lets automated provers remain effective in large background theories.

ABSTRACT. The Mizar Mathematical Library (MML) is a collection of mathematical documents formalized by the Mizar system. Visualizing the interrelationships among the MML articles can illuminate their structure and connections, but the scale and intricacy pose significant challenges. In our research, we introduce a method to illustrate these MML dependencies: we sort the MML articles according to the classifications in the Encyclopedic Dictionary of Mathematics. Moreover, we are exploring the feasibility of utilizing generative AI to automate this sorting process, aiming to lessen the need for manual labor. Finally, we also discuss a new algorithm for rendering categorized dependency graphs.

ABSTRACT. Base ten blocks used together with a grid can provide a consistent environment for modelling place value as well as arithmetic operations, such as addition, subtraction, regrouping and decomposition, which is particularly beneficial for students who struggle with mathematics. However, their physical use requires extensive teacher training and almost constant teacher supervision of a student. Digital interactions with base ten blocks and a grid allow for independent work and therefore enormous scalability of math interventions. This exploratory research aims to evaluate the feasibility of this digitisation process and identify the main challenges that need to be overcome to maintain or even improve on effectiveness of base ten blocks on a grid.

ABSTRACT. One aspect of naturalness in natural language proof texts is the limitation of objects to a cognitively manageable number or their grouping in a limited number of aggregates in each part of a proof. More precisely, we should talk about "reference markers" instead of "objects", abstracting from the ontological structure we are referring to. Here, the term "reference marker" is used in a sense that any (generalized) quantifier introduces one or two new reference markers which can be referenced in the following text. In this sense, when talking about "every group g" one new reference marker g and - if not yet introduced into the discourse - a discourse marker for the set of groups are added to the discourse, only.

A common means of grouping discourse markers in formal notations of natural language proof texts are typographical means and diacritics, cf. the notations for a straight line through the point A and B, a ray starting at A and running through B, a line segment between A und B, and its length. Or consider how functions and their derivatives and antiderivatives are usually written.

Another technique of grouping related objects is the use of ambiguous, particularly polysemous expressions the readings of which are related metonymically. Polysemy means an ambiguity where the different meanings of an expression are conceptually related, like "height" meaning a dimension of measure and a geographical place. A big portion of polysemous readings are based on metonymy. So, e.g., "school" could be used to refer to an institution or to a building which hosts this institution in the same text. Both meanings are ontologically different, but are connected by a "contiguous" relation (cf. Panther/Radden eds. 1999), here the place where an institution is situated. Most cases of metonymy can be explained by a small set of contiguous relations. Commonly, language users become aware of such cases of polysemy in very few contexts.

In a similar metonymical fashion mathematical terms referring to results of arithmetical operations as e.g. "sum" or "product" (cf. (1)) can also refer to the expressions of the arithmetical operations or to various levels of abstraction from the expressions (e.g. by abstracting from commutative or associative transformations of the expressions), cf (2).

(1) The sum of x and y is not divible by 3. (2) r is the square-free part of the product of the numbers in M.

Mathematical notation is sometimes designed to address these levels of abstraction e.g. by leaving open the exact associative structure of an expression, cf.

(3) a+b+c

Another source of polysemy is the implicit introduction of plural entities, i.e. entities like sets, sequences etc. comprising more than one member (see Nouwen 2015, Cramer/Schröder 2012 and Schröder in print). In a sentence like

(4) a, b and c are P.

the predicate P can be applied to a, b and c respectively (distributive interpretation) or to a plural entity formed by a, b and c (collective interpretation), as e.g. the set {a,b,c}. Even more interpretations get possible if further quantifications come into play.

(5) For all i, a_i, b_i and c_i are P.

could have a purely distributive interpretation, but also a collective interpretation for the plural entities constituted by a_i, b_i and c_i for each i, and collective interpretations for plural entities like {a_i, b_i, c_i | i} or {{a_i, b_i, c_i} | i}. In many proof texts the natural language mechanism of implicitly forming plural entities is used very effectively.

In my contribution I will argue that the notational means to group reference markers and the metonymical uses of mathematical terms are essential for keeping natural language mathematical proofs readable and natural.

References

• Carl, Merlin/Cramer, Marcos/Fisseni, Bernhard/Sarikaya, Deniz/Schröder, Bernhard (2021). How to Frame Understanding in Mathematics: A Case Study Using Extremal Proofs. In: Axiomathes 31, 649–676. DOI: 10.1007/s10516-021-09552-9.
• Cramer, Marcos (2013): Proof-checking mathematical texts in controlled natural language. PhD Thesis. Rheinische Friedrich-Wilhelms-Universität Bonn. https://hdl.handle.net/20.500.11811/5780 (accessed on 1 Jun 2023).
• Cramer, Marcos/Fisseni, Bernhard/Koepke, Peter/Kühlwein, Daniel/Schröder, Bernhard/Veldman, Jip (2010): The Naproche Project. Controlled Natural Language Proof Checking of Mathematical Texts. In: Fuchs, Norbert E. (Ed.) Controlled Natural Language. CNL 2009. (= Lecture Notes in Computer Science 5972. Berlin, Heidelberg: Springer, 170-186. DOI: 10.1007/978-3-642-14418-9_11.
• Cramer, Marcos/Schröder, Bernhard (2012). Interpreting Plurals in the Naproche CNL. In: Rosner, Michael/Fuchs, Norbert E. (Eds.): Controlled Natural Language. CNL 2010. (= Lecture Notes in Computer Science 7175). Berlin, Heidelberg: Springer, S. 43-52. DOI: 10.1007/978-3-642-31175-8_3.
• Fisseni, Bernhard/Sarikaya, Deniz/Schmitt, Martin/Schröder, Bernhard (2019): How to frame a mathematician. In: Centrone, Stefania/Sarikaya, Deniz/Kant, Deborah (Eds.): Reflections on the foundation of mathematics. Heidelberg: Springer, 415-434.
• Nouwen, R. (2015): Plurality. In Dekker, Paul/Aloni, Maria (Eds.): Cambridge handbook of semantics. Cambridge: Cambridge University Press.
• Panther, Klaus-Uwe/Radden, Günter (Eds., 1999): Metonymy in Language and Thought. Amsterdam: John Benjamins Publishing.
• Schröder, Bernhard (in print): Induktiv oder intuitiv? Die Gewinnung von Frames aus mathematischen Beweistexten

ABSTRACT. Freek Wiedijk's webpage "Formalizing 100 Theorems" [1] is sometimes considered a benchmark for formalizations in interactive proof systems. It also provides immediate comparisons between proof styles in different systems.

In our talk we present a formalization in the Naproche Natural Proof Checker [2, 3] of sets, numbers and about 10 theorems from Wiedijk's list. The formalization is part of the Isabelle 2023 release together with a pdf-printout. Naproche formalizations aim at natural mathematical readability: texts are written in a LaTeX source format that compiles to pdf documents which read like standard mathematics. Strong automatic theorem provers are employed to achieve textbook-like proof granularities.

Naproche's input language ForTheL [4] (for Formula Theory Language) is a controlled natural language based on patterns of tokens. The Naproche system parses an input text into an incomplete proof tree of first-order statements, where leaves correspond to axiomatic assumptions, and other nodes are supposed to follow logically from premises higher up in the tree. The system reads through the proof tree and checks statements for type correctness and provability from their premises. These checks are mainly done by external ATPs like E or Vampire. In line with the standard foundations of mathematics in first-order logic and set theory, linguistic types like "natural number" or "function" are interpreted as type guards. Sets (and classes) can be formed by abstraction terms, obeying set existence axioms.

Naproche is a component of the Isabelle prover platform [5]. After downloading and installing Isabelle, Naproche is immediately available and will automatically check .ftl.tex files opened in the Isabelle editor. Isabelle/Naproche ships with a couple of example files ranging from small demos to larger mathematical developments. The present formalization is included as the example file sets_and_numbers.ftl.tex.

In the formalization, set theory is developed up to the well-known theorems of Cantor and Cantor-Schröder-Bernstein which are #63 and #25 on Wiedijk's list. The standard number systems are introduced "top-down": we postulate field axioms for the real numbers and then introduce the subsystems of rational, integer and natural numbers. Interestingly, the principle of mathematical induction (#74) follows from the supremum principle for real numbers. Using induction we prove the summation formulas for finite geometric (#66) and arithmetic series (#68), and the number of subsets of finite sets (#52). After the introduction of division and primes in the natural numbers we prove the correctness of Euclid's algorithm (#69), Bezout's theorem (#60), the irrationality of \sqrt{2} (#1) and the infinitude of primes (#11). We conclude with the denumerability of the rational numbers (#3) and the uncountability of the real continuum (#22). Overall, the formalization could be used in a seminar which teaches natural and formal proving with Naproche whilst recapitulating basic and interesting facts about sets and numbers.

[1] https://www.cs.ru.nl/~freek/100/

[2] https://naproche.github.io/index.html

[3] Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Makarius Wenzel: The Isabelle/Naproche Natural Language Proof Assistant. In: Automated Deduction – CADE 28: 28th International Conference on Automated Deduction (Proceedings), 2021, pp. 614–624.

[4] Andrei Paskevich: The syntax and semantics of the ForTheL language. 2007. URL: http://nevidal.org/download/forthel.pdf

[5] https://isabelle.in.tum.de/

ABSTRACT. Naproche Demonstration