Reseña: Formalizing divisibility rules as a student case study

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Mizar sobre aritmética titulado Formalizing divisibility rules as a student case study.

Su autor es Adam Naumowicz (de la Univ. de Białystok en Polonia).

Su resumen es

We would like to present some results of a student case study administered as a part of an interactive theorem proving elective course for computer science students. The students’ task was to prove in Mizar the divisibility rules for selected primes based on the decimal representation of natural numbers. The formalized proofs were quite elementary, so a project like this could be carried out by a group of students without particularly strong mathematical background. In this paper we give a short overview of definitions that had to be introduced for the case study and present the way the divisibility rules were eventually formulated by the students. After that we discuss an example of a more interesting proof case, i.e. the divisibility by 11 rule.

El trabajo se ha presentado en CICM 2015 (the 8th Conference on Intelligent Computer Mathematics).

Polygonal numbers in Mizar

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Mizar titulado Polygonal numbers in Mizar.

Su autor es Adam Grabowski (de la Universidad de Białystok, Polonia).

Su resumen es

In the article the formal characterization of triangular numbers (famous from [14] and words “EYPHKA! num = ∆ + ∆ + ∆”) [16] is given. Our primary aim was to formalize one of the items (42) from Wiedijk’s Top 100 Mathematical Theorems list, namely that the sequence of sums of reciprocals of triangular numbers converges to 2 and this Mizar representation was written in 2007. As the Mizar language evolved and attributes with arguments were implemented, we decided to extend these lines and we characterized polygonal numbers.

We formalized centered polygonal numbers, the connection between triangular and square numbers, and also some equalities involving Mersenne primes and perfect numbers. We gave also explicit formula to obtain from the polygonal number its ordinal index. Also selected congruences modulo 10 were enumerated. Our work basically covers the Wikipedia item for triangular numbers and
the Online Encyclopedia of Integer Sequences (http://oeis.org/A000217).

An interesting related result [15] could be the proof of Lagrange’s four-square theorem or Fermat’s polygonal number theorem [30].

El artículo se publicará en la revista Formalized Mathematics.

Reseña: Developing an auction theory toolbox

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Developing an auction theory toolbox.

Sus autores son Christoph Lange, Colin Rowat, Wolfgang Windsteiger y Manfred Kerber.

Su resumen es

Auctions allocate trillions of dollars in goods and services every year. Auction design can have significant consequences, but its practice outstrips theory. We seek to advance auction theory with help from mechanised reasoning. To that end we are developing a toolbox of formalised representations of key facts of auction theory, which will allow auction designers to have relevant properties of their auctions machine-checked. As a first step, we are investigating the suitability of different mechanised reasoning systems (Isabelle, Theorema, and TPTP) for reproducing a key result of auction theory: Vickrey’s celebrated 1961 theorem on the properties of second price auctions – the foundational result in modern auction theory. Based on our formalisation experience, we give tentative recommendations on what system to use for what purpose in auction theory, and outline further steps towards a complete auction theory toolbox.

El trabajo se presentó en la AISB Convention 2013.

Los códigos de las correspondientes teorías se encuentran Auction Theory Toolbox (ATT). Contiene los códigos de las formalizaciones en CASL, Isabelle, Mizar y Theorema.

Reseña: AI over large formal knowledge bases: The first decade

PorJosé A. Alonso

Se ha publicado un artículo sobre aplicaciones de la inteligencia artificial a la demostración automática de teoremas titulado AI over large formal knowledge bases: The first decade.

Su autor es Josef Urban (de la Univ. de Nimega, Países Bajos) y lo presentará mañana en el ARW2013 (20th Automated Reasoning Workshop).

Su resumen es

In March 2003, the first version of the Mizar Problems for Theorem Proving (MpTP) was released. In the past ten years, such large formal knowledge bases have started to provide an interesting playground for combining deductive and inductive AI methods. The talk will discuss three related areas of application in which machine learning and general AI have been recently experimented with: (i) premise selection for theorem proving over large formal libraries built with systems like Mizar, HOL Light, and Isabelle (ii) advising and tuning first-order automated theorem provers such as E and leanCoP, and (iii) building larger inductive/deductive AI systems such as MaLARea. Here I focus on the wider motivation for this work.

Reseña: Formalization of real analysis: A survey of proof assistants and libraries

PorJosé A. Alonso

Se ha publicado un artículo sobre razonamiento formalizado titudado Formalization of real analysis: A survey of proof assistants and libraries.

Sus autores son Sylvie Boldo, Catherine Lelay y Guillaume Melquiond.

Su resumen es

In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability, and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle/HOL, Mizar, ProofPower-HOL, and PVS. We have also accounted for large developments that play a similar role or extend standard libraries: ACL2(r) for ACL2, C-CoRN/MathClasses for Coq, and the NASA PVS library. This survey presents how real numbers have been defined in these various provers and how the notions of real analysis described above have been formalized. We also look at the proof automations these systems provide for real analysis.