## Summary

## Summary

Binary representation of integers , and arithmetic operations on them have already been introduced in Mizar Mathematical Library , , , ]. However, these articles formalize the notion of integers as mapped into a certain length tuple of boolean values.

In this article we formalize, by means of Mizar system , , the binary representation of natural numbers which maps ℕ into bitstreams.

## Summary

In this article we formalize the Bertrand’s Ballot Theorem based on [17]. Suppose that in an election we have two candidates: *A* that receives *n* votes and *B* that receives *k* votes, and additionally *n ≥ k*. Then this theorem states that the probability of the situation where *A* maintains more votes than *B* throughout the counting of the ballots is equal to (*n − k*)/(*n* + *k*).

This theorem is item #30 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.

## Summary

Formalization of a part of . Unfortunately, not all is possible to be formalized. Namely, in the paper there is a mistake in the proof of Lemma 3. It states that there exists *x* ∈ *M*
_{1} such that *M*
_{1}(*x*) > *N*
_{1}(*x*) and (∀*y* ∈ *N*
_{1})*x* ⊀ *y*. It should be *M*
_{1}(*x*) ⩾ *N*
_{1}(*x*). Nevertheless we do not know whether *x* ∈ *N*
_{1} or not and cannot prove the contradiction. In the article we referred to , and .

## Summary

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 [], [], 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 [].“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.”

## Summary

We start with the definition of stopping time according to [], p.283. We prove, that different definitions for stopping time can coincide. We give examples of stopping time using constant-functions or functions defined with the operator max or min (defined in [], pp.37–38). Finally we give an example with some given filtration. Stopping time is very important for stochastic finance. A stopping time is the moment, where a certain event occurs ([], p.372) and can be used together with stochastic processes ([], p.283). Look at the following example: we install a function ST: {1,2,3,4} → {0, 1, 2} ∪ {+∞}, we define:

a. ST(1)=1, ST(2)=1, ST(3)=2, ST(4)=2.

b. The set {0,1,2} consists of time points: 0=now,1=tomorrow,2=the day after tomorrow.

We can prove:

c. {w, where w is Element of Ω: ST.w=0}=∅ & {w, where w is Element of Ω: ST.w=1}={1,2} & {w, where w is Element of Ω: ST.w=2}={3,4} and

ST is a stopping time.

We use a function Filt as Filtration of {0,1,2}, Σ where Filt(0)=Ω* _{now}*, Filt(1)=Ω

_{fut}_{1}and Filt(2)=Ω

_{fut}_{2}. From a., b. and c. we know that:

d. {w, where w is Element of Ω: ST.w=0} in Ω* _{now}* and

{w, where w is Element of Ω: ST.w=1} in Ω_{fut}_{1} and

{w, where w is Element of Ω: ST.w=2} in Ω_{fut}_{2}.

The sets in d. are events, which occur at the time points 0(=now), 1(=tomorrow) or 2(=the day after tomorrow), see also [], p.371. Suppose we have ST(1)=+∞, then this means that for 1 the corresponding event never occurs.

As an interpretation for our installed functions consider the given adapted stochastic process in the article [].

ST(1)=1 means, that the given element 1 in {1,2,3,4} is stopped in 1 (=tomorrow). That tells us, that we have to look at the value *f*
_{2}(1) which is equal to 80. The same argumentation can be applied for the element 2 in {1,2,3,4}.

ST(3)=2 means, that the given element 3 in {1,2,3,4} is stopped in 2 (=the day after tomorrow). That tells us, that we have to look at the value *f*
_{3}(3) which is equal to 100.

ST(4)=2 means, that the given element 4 in {1,2,3,4} is stopped in 2 (=the day after tomorrow). That tells us, that we have to look at the value *f*
_{3}(4) which is equal to 120.

In the real world, these functions can be used for questions like: when does the share price exceed a certain limit? (see [], p.372).

## Summary

In the article we formalize in the Mizar system [] preliminary facts needed to prove the Basel problem [, ]. Facts that are independent from the notion of structure are included here.

## Summary

This article provides a formalized proof of the so-called “the four-square theorem”, namely any natural number can be expressed by a sum of four squares, which was proved by Lagrange in 1770. An informal proof of the theorem can be found in the number theory literature, e.g. in [14], [1] or [23].

This theorem is item #19 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.

## Summary

In the article we formalized in the Mizar system [] the Vieta formula about the sum of roots of a polynomial *a _{n}x^{n}* +

*a*

_{n−}_{1}

*x*

^{n−}^{1}+

*···*+

*a*

_{1}

*x*+

*a*

_{0}defined over an algebraically closed field. The formula says that

*x*

_{1},

*x*

_{2},…,

*x*are (not necessarily distinct) roots of the polynomial []. In the article the sum is denoted by

_{n}## Summary

In this article, we formalize in the Mizar system [, ] some properties of vector spaces over a ring. We formally prove the first isomorphism theorem of vector spaces over a ring. We also formalize the product space of vector spaces. ℤ-modules are useful for lattice problems such as LLL (Lenstra, Lenstra and Lovász) [] base reduction algorithm and cryptographic systems [, ].