Abstract
In this article we construct formally the Pascal’s triangle using Mizar proof assistant. Using the same techniques, we show some similar constructions based on integer sequences. We also prove Lucas’s theorem providing useful registrations of clusters to enable more automation in calculations.
Language: English
Page range: 235 - 245
Accepted on: Dec 24, 2024
Published on: Dec 31, 2024
Published by: University of Białystok
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Keywords:
Related subjects:
© 2024 Rafał Ziobro, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.