5 papers
IntSeqBERT: Learning Arithmetic Structure in OEIS via Modulo-Spectrum Embeddings
Kazuhisa Nakasho
Integer sequences in the OEIS span values from single-digit constants to astronomical factorials and exponentials, making prediction challenging for standard tokenised models that…
Remote Verification System for Mizar Integrated with Emwiki
Toshiki Kai, Yuta Teruya, Kazuhisa Nakasho
In this paper, we present a remote verification environment for Mizar and its integration with a web platform. Although a VSCode extension for Mizar is already available, it requir…
The Tight Upper Bound for the Size of Single Deletion Error Correcting Codes in Dimension 11
Kazuhisa Nakasho, Manabu Hagiwara, Austin Anderson +1
A single deletion error correcting code (SDECC) is a set of fixed-length sequences consisting of two types of symbols, 0 and 1, such that the original sequence can be recovered for…
An Integrated Web Platform for the Mizar Mathematical Library
Hideharu Furushima, Daichi Yamamichi, Seigo Shigenaka +2
This paper reports on the development of a Web platform to host the Mizar Mathematical Library (MML). In recent years, the size of formalized mathematical libraries has been drasti…
Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
Kazuhisa Nakasho, Yasunari Shidama
The purpose of this project is to collect symbol information in the Mizar Mathematical Library and manipulate it into practical and organized documentation. Inspired by the MathWik…