29 citations · 54 across the 8 of their papers we have counts for
11 papers · 1 filter
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers
Karol Pąk, Cezary Kaliszyk
The proper class of Conway's surreal numbers forms a rich totally ordered algebraically closed field with many arithmetic and algebraic properties close to those of real numbers, t…
Lash 1.0 (System Description)
Chad E. Brown, Cezary Kaliszyk
Lash is a higher-order automated theorem prover created as a fork of the theorem prover Satallax. The basic underlying calculus of Satallax is a ground tableau calculus whose rules…
JEFL: Joint Embedding of Formal Proof Libraries
Qingxiang Wang, Cezary Kaliszyk
The heterogeneous nature of the logical foundations used in different interactive proof assistant libraries has rendered discovery of similar mathematical concepts among them diffi…
Online Machine Learning Techniques for Coq: A Comparison
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski +3
We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin f…
A Survey of Languages for Formalizing Mathematics
Cezary Kaliszyk, Florian Rabe
In order to work with mathematical content in computer systems, it is necessary to represent it in formal languages. Ideally, these are supported by tools that verify the correctne…
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk +1
In this paper we share several experiments trying to automatically translate informal mathematics into formal mathematics. In our context informal mathematics refers to human-writt…