<abstract xmlns="http://www.w3.org/1999/xhtml">The real projective plane has been formalized in Isabelle/HOL by Timothy Makarios [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_013_w2aab2b8c14b1b7b1ab1ac13Aa">13</xref>] and in Coq by Nicolas Magaud, Julien Narboux and Pascal Schreck [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_012_w2aab2b8c14b1b7b1ab1ac12Aa">12</xref>].Some definitions on the real projective spaces were introduced early in the Mizar Mathematical Library by Wojciech Leonczuk [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_009_w2aab2b8c14b1b7b1ab1ab9Aa">9</xref>], Krzysztof Prazmowski [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_010_w2aab2b8c14b1b7b1ab1ac10Aa">10</xref>] and by Wojciech Skaba [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_018_w2aab2b8c14b1b7b1ab1ac18Aa">18</xref>].In this article, we check with the Mizar system [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_004_w2aab2b8c14b1b7b1ab1ab4Aa">4</xref>], some properties on the determinants and the Grassmann-Plücker relation in rank 3 [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_002_w2aab2b8c14b1b7b1ab1ab2Aa">2</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_001_w2aab2b8c14b1b7b1ab1ab1Aa">1</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_007_w2aab2b8c14b1b7b1ab1ab7Aa">7</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_016_w2aab2b8c14b1b7b1ab1ac16Aa">16</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_017_w2aab2b8c14b1b7b1ab1ac17Aa">17</xref>].Then we show that the projective space induced (in the sense defined in [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_009_w2aab2b8c14b1b7b1ab1ab9Aa">9</xref>]) by ℝ3 is a projective plane (in the sense defined in [<xref ref-type="bibr" rid="j_forma-2016-0020_ref_010_w2aab2b8c14b1b7b1ab1ac10Aa">10</xref>]).Finally, in the real projective plane, we define the homography induced by a 3-by-3 invertible matrix and we show that the images of 3 collinear points are themselves collinear.</abstract>

Homography in ℝℙ

<abstract xmlns="http://www.w3.org/1999/xhtml">In this article, the basic existence theorem of Riemann-Stieltjes integral is formalized. This theorem states that if <italic>f</italic> is a continuous function and <italic>ρ</italic> is a function of bounded variation in a closed interval of real line, <italic>f</italic> is Riemann-Stieltjes integrable with respect to <italic>ρ</italic>. In the first section, basic properties of real finite sequences are formalized as preliminaries. In the second section, we formalized the existence theorem of the Riemann-Stieltjes integral. These formalizations are based on [<xref ref-type="bibr" rid="j_forma-2016-0021_ref_015_w2aab2b8b1b1b7b1ab1ac15Aa">15</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0021_ref_012_w2aab2b8b1b1b7b1ab1ac12Aa">12</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0021_ref_010_w2aab2b8b1b1b7b1ab1ac10Aa">10</xref>], and [<xref ref-type="bibr" rid="j_forma-2016-0021_ref_011_w2aab2b8b1b1b7b1ab1ac11Aa">11</xref>].</abstract>

The Basic Existence Theorem of Riemann-Stieltjes Integral

<abstract xmlns="http://www.w3.org/1999/xhtml">While discussing the sum of consecutive powers as a result of division of two binomials W.W. Sawyer [<xref ref-type="bibr" rid="j_forma-2016-0022_ref_012_w2aab2b8b8b1b7b1ab1ac12Aa">12</xref>] observes
<disp-quote>“It is a curious fact that most algebra textbooks give our ast result twice. It appears in two different chapters and usually there is no mention in either of these that it also occurs in the other. The first chapter, of course, is that on factors. The second is that on geometrical progressions. Geometrical progressions are involved in nearly all financial questions involving compound interest – mortgages, annuities, etc.”</disp-quote>
It’s worth noticing that the first issue involves a simple arithmetical division of 99...9 by 9. While the above notion seems not have changed over the last 50 years, it reflects only a special case of a broader class of problems involving two variables. It seems strange, that while binomial formula is discussed and studied widely [<xref ref-type="bibr" rid="j_forma-2016-0022_ref_007_w2aab2b8b8b1b7b1ab1ab7Aa">7</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0022_ref_008_w2aab2b8b8b1b7b1ab1ab8Aa">8</xref>], little research is done on its counterpart with all coefficients equal to one, which we will call here the subnomial. The study focuses on its basic properties and applies it to some simple problems usually proven by induction [<xref ref-type="bibr" rid="j_forma-2016-0022_ref_006_w2aab2b8b8b1b7b1ab1ab6Aa">6</xref>].</abstract>

On Subnomials

<abstract xmlns="http://www.w3.org/1999/xhtml">In this article we prove the Leibniz series for <italic>π</italic> which states that
<disp-formula><alternatives><graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2016-0023_eq_001.png"></graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mfrac><mi>π</mi><mn>4</mn></mfrac><mo>=</mo><mstyle displaystyle="true"><munderover><mo>∑</mo><mrow><mi>n</mi><mo>=</mo><mn>0</mn></mrow><mi>∞</mi></munderover><mrow><mfrac><mrow><msup><mrow><mrow><mo>(</mo><mrow><mo>−</mo><mn>1</mn></mrow><mo>)</mo></mrow></mrow><mi>n</mi></msup></mrow><mrow><mn>2</mn><mo>⋅</mo><mi>n</mi><mo>+</mo><mn>1</mn></mrow></mfrac><mo>.</mo></mrow></mstyle></math><tex-math>$${\pi \over 4} = \sum\limits_{n = 0}^\infty {{{\left( { - 1} \right)^n } \over {2 \cdot n + 1}}.} $$</tex-math></alternatives></disp-formula>The formalization follows K. Knopp [<xref ref-type="bibr" rid="j_forma-2016-0023_ref_008_w2aab2b8b2b1b7b1ab1ab8Aa">8</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0023_ref_001_w2aab2b8b2b1b7b1ab1ab1Aa">1</xref>] and [<xref ref-type="bibr" rid="j_forma-2016-0023_ref_006_w2aab2b8b2b1b7b1ab1ab6Aa">6</xref>]. <italic>Leibniz’s Series for Pi</italic> is item #26 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="http://www.cs.ru.nl/F.Wiedijk/100/">http://www.cs.ru.nl/F.Wiedijk/100/</ext-link>.</abstract>

Leibniz Series for <italic>π</italic>

<abstract xmlns="http://www.w3.org/1999/xhtml">This article introduces propositional logic as a formal system ([<xref ref-type="bibr" rid="j_forma-2016-0024_ref_014_w2aab2b8b9b1b7b1ab1ac14Aa">14</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0024_ref_010_w2aab2b8b9b1b7b1ab1ac10Aa">10</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0024_ref_011_w2aab2b8b9b1b7b1ab1ac11Aa">11</xref>]). The formulae of the language are as follows <italic>φ</italic> ::= ⊥ | <italic>p</italic> | <italic>φ</italic> → <italic>φ</italic>. Other connectives are introduced as abbrevations. The notions of model and satisfaction in model are defined. The axioms are all the formulae of the following schemes
<list list-type="bullet"><list-item><italic>α</italic> ⇒ (<italic>β</italic> ⇒ <italic>α</italic>),</list-item><list-item>(<italic>α</italic> ⇒ (<italic>β</italic> ⇒ <italic>γ</italic>)) ⇒ ((<italic>α</italic> ⇒ <italic>β</italic>) ⇒ (<italic>α</italic> ⇒ <italic>γ</italic>)),</list-item><list-item>(¬<italic>β</italic> ⇒ ¬<italic>α</italic>) ⇒ ((¬<italic>β</italic> ⇒ <italic>α</italic>) ⇒ <italic>β</italic>).</list-item></list>
Modus ponens is the only derivation rule. The soundness theorem and the strong completeness theorem are proved. The proof of the completeness theorem is carried out by a counter-model existence method. In order to prove the completeness theorem, Lindenbaum’s Lemma is proved. Some most widely used tautologies are presented.</abstract>

The Axiomatization of Propositional Logic

<abstract xmlns="http://www.w3.org/1999/xhtml">This article provides definitions and examples upon an integral element of unital commutative rings. An algebraic number is also treated as consequence of a concept of “integral”. Definitions for an integral closure, an algebraic integer and a transcendental numbers [<xref ref-type="bibr" rid="j_forma-2016-0025_ref_014_w2aab2b8b6b1b7b1ab1ac14Aa">14</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0025_ref_001_w2aab2b8b6b1b7b1ab1ab1Aa">1</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0025_ref_010_w2aab2b8b6b1b7b1ab1ac10Aa">10</xref>] and [<xref ref-type="bibr" rid="j_forma-2016-0025_ref_007_w2aab2b8b6b1b7b1ab1ab7Aa">7</xref>] are included as well. As an application of an algebraic number, this article includes a formal proof of a ring extension of rational number field ℚ induced by substitution of an algebraic number to the polynomial ring of ℚ[<italic>x</italic>] turns to be a field.</abstract>

Algebraic Numbers

<abstract xmlns="http://www.w3.org/1999/xhtml">This article formalizes the proof of Niven’s theorem [<xref ref-type="bibr" rid="j_forma-2016-0026_ref_012_w2aab2b8c11b1b7b1ab1ac12Aa">12</xref>] which states that if <italic>x/π</italic> and <italic>sin</italic>(<italic>x</italic>) are both rational, then the sine takes values 0, ±1/2, and ±1. The main part of the formalization follows the informal proof presented at Pr∞fWiki (<ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://proofwiki.org/wiki/Niven’s_Theorem#Source_of_Name">https://proofwiki.org/wiki/Niven’s_Theorem#Source_of_Name</ext-link>). For this proof, we have also formalized the rational and integral root theorems setting constraints on solutions of polynomial equations with integer coefficients [<xref ref-type="bibr" rid="j_forma-2016-0026_ref_008_w2aab2b8c11b1b7b1ab1ab8Aa">8</xref>, <xref ref-type="bibr" rid="j_forma-2016-0026_ref_009_w2aab2b8c11b1b7b1ab1ab9Aa">9</xref>].</abstract>

Institute of Informatics, University of Białystok,

Niven’s Theorem

AHEAD OF PRINT

Volume 31 (2023): Issue 1 (September 2023)

Volume 30 (2022): Issue 4 (December 2022)

Volume 30 (2022): Issue 3 (October 2022)

Volume 30 (2022): Issue 2 (July 2022)

Volume 30 (2022): Issue 1 (April 2022)

Volume 29 (2021): Issue 4 (December 2021)

Volume 29 (2021): Issue 3 (October 2021)

Volume 29 (2021): Issue 2 (July 2021)

Volume 29 (2021): Issue 1 (April 2021)

Volume 28 (2020): Issue 4 (December 2020)

Volume 28 (2020): Issue 3 (October 2020)

Volume 28 (2020): Issue 2 (July 2020)

Volume 28 (2020): Issue 1 (April 2020)

Volume 27 (2019): Issue 4 (December 2019)

Volume 27 (2019): Issue 3 (October 2019)

Volume 27 (2019): Issue 2 (July 2019)

Volume 27 (2019): Issue 1 (April 2019)

Volume 26 (2018): Issue 4 (December 2018)

Volume 26 (2018): Issue 3 (October 2018)

Volume 26 (2018): Issue 2 (July 2018)

Volume 26 (2018): Issue 1 (April 2018)

Volume 25 (2017): Issue 4 (December 2017)

Volume 25 (2017): Issue 3 (October 2017)

Volume 25 (2017): Issue 2 (July 2017)

Volume 25 (2017): Issue 1 (March 2017)

Volume 24 (2016): Issue 4 (December 2016)

Volume 24 (2016): Issue 3 (September 2016)

Volume 24 (2016): Issue 2 (June 2016)

Volume 24 (2016): Issue 1 (March 2016)

Volume 23 (2015): Issue 4 (December 2015)

Volume 23 (2015): Issue 3 (September 2015)

Volume 23 (2015): Issue 2 (June 2015)

Volume 23 (2015): Issue 1 (March 2015)

Volume 22 (2014): Issue 4 (December 2014)

Volume 22 (2014): Issue 3 (September 2014)

Volume 22 (2014): Issue 2 (June 2014) Special Issue: 25 years of the Mizar Mathematical Library

Volume 22 (2014): Issue 1 (March 2014)

Volume 21 (2013): Issue 4 (December 2013)

Volume 21 (2013): Issue 3 (October 2013)

Volume 21 (2013): Issue 2 (June 2013)

Volume 21 (2013): Issue 1 (January 2013)

Volume 20 (2012): Issue 4 (December 2012)

Volume 20 (2012): Issue 3 (September 2012)

Volume 20 (2012): Issue 2 (December 2012)

Volume 20 (2012): Issue 1 (January 2012)

Volume 19 (2011): Issue 4 (December 2011)

Volume 19 (2011): Issue 3 (September 2011)

Volume 19 (2011): Issue 2 (June 2011)

Volume 19 (2011): Issue 1 (March 2011)

Volume 18 (2010): Issue 4 (January 2010)

Volume 18 (2010): Issue 3 (September 2010)

Volume 18 (2010): Issue 2 (June 2010)

Volume 18 (2010): Issue 1 (March 2010)

Volume 17 (2009): Issue 4 (December 2009)

Volume 17 (2009): Issue 3 (September 2009)

Volume 17 (2009): Issue 2 (June 2009)

Volume 17 (2009): Issue 1 (March 2009)

Volume 16 (2008): Issue 4 (December 2008)

Volume 16 (2008): Issue 3 (January 2008)

Volume 16 (2008): Issue 2 (June 2008)

Volume 16 (2008): Issue 1 (March 2008)

Volume 15 (2007): Issue 4 (December 2007)

Volume 15 (2007): Issue 3 (September 2007)

Volume 15 (2007): Issue 2 (June 2007)

Volume 15 (2007): Issue 1 (January 2007)

Volume 14 (2006): Issue 4 (December 2006)

Volume 14 (2006): Issue 3 (September 2006)

Volume 14 (2006): Issue 2 (June 2006)

Volume 14 (2006): Issue 1 (March 2006)

Formalized Mathematics

  Pioneering Journal in the field of formalized and mechanically checked mathematics. Excellent articles on latest research in formal methods and computer-checked mathematics. Full-length original research articles in English. Archival issues available at the journal's home page fm.mizar.org/.   To build a uniform and extensible computer-checked repository of mathematical knowledge.  Reconstruction of mathematics based on mechanization of mathematical reasoning.  To check a wide range of mathematical theorems using a computer in an automatic fashion.  General mathematics: especially topology, lattice theory, functional analysis.  Applications: computer-aided verification of software and hardware, computer-aided teaching of mathematics.   Why subscribe and read   Pioneering source of high quality research in formalized and mechanically checked mathematics.  The oldest journal in the field, a medium for the publication of research reporting pioneering findings of broad mathematical significance that are likely to advance the direction and thinking of the field.  Long-term experience in publishing original articles on mechanizing mathematics and various aspects of automated reasoning, since 1990.   Why submit   Fair and constructive peer review by international experts in the field (three referees are designated for the assessment of each manuscript) - double-blind review process.  New publishing technology: articles automatically translated from a formal language into English and automatically typeset, available in both forms - electronic and printed.  Articles abstracted by online indexing services and databases.   Rejection Rate   59% of submitted articles.  The rejection percentage is described in detail in the following paper, pp.239-240: dx.doi.org/10.1007/978-3-540-73086-6_20 Archiving  Sciendo archives the contents of this journal in Portico - digital long-term preservation service of scholarly books, journals and collections.  Plagiarism Policy  The editorial board is participating in a growing community of Similarity Check System's users in order to ensure that the content published is original and trustworthy. Similarity Check is a medium that allows for comprehensive manuscripts screening, aimed to eliminate plagiarism and provide a high standard and quality peer-review process. Back Issues fm.mizar.org/   Other Files  Addenda 2008Formalized Mathematics Bibliography File.Formalized Mathematics External Bibliography File.  "In years: 2016-2017, the English version of Formalized Mathematics was financed under agreements 548/P-DUN/2016 and 548/1/P-DUN/2016 with the funds from the Polish Minister of Science and Higher Education for the dissemination of science." 