An Integrated Web Platform for the Mizar Mathematical Library Hideharu Furushima1 Daichi Yamamichi1 Seigo Shigenaka1 Kazuhisa

2025-04-27 0 0 251.55KB 6 页 10玖币

侵权投诉

An Integrated Web Platform for the Mizar

Mathematical Library

Hideharu Furushima1, Daichi Yamamichi1, Seigo Shigenaka1, Kazuhisa

Nakasho1,3[0000−0003−1110−4342], and Katsumi Wasaki2

1Yamaguchi University, Yamaguchi, Japan

{b089vgv,a102vgu,a085vgu,nakasho}@yamaguchi-u.ac.jp

2Shinshu University, Nagano, Japan {wasaki}@cs.shinshu-u.ac.jp

3corresponding author

Abstract. 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 drastically increasing, and

this has led to a growing demand for tools that support eﬃcient and com-

prehensive browsing, searching, and annotation of these libraries. This

platform implements a Wiki function to add comments to the HTML-

ized MML, three types of search function (article, symbol, and theorem),

and a function to show the dependency graph of the MML. This plat-

form is designed with consistency, scalability, and interoperability as top

priorities for long-term use.

Keywords: mathematical knowledge management ·Mizar Mathemati-

cal Library ·QED manifesto ·Web service.

1 Introduction

Many systems have been proposed to improve the browsability and searchabil-

ity of formalized mathematical libraries. The MathWiki Project4aims to im-

prove the readability of formalized mathematical libraries and make them ac-

cessible to wider communities. A Wiki for Mizar [17], Large Formal Wikis for

Coq/CoRN [2], and Agora System for Flyspeck Project [16] were proposed in

the MathWiki project. However, since the MathWiki Project was terminated in

2014, its contents cannot follow the libraries’ updates. ProofWiki [19] and the

Lean Mathematical Library [8] accumulate mathematical libraries and convert

them into highly readable HTML documents. However, these two systems do not

collaborate with advanced search engines or graphical tools to visualize library

dependencies.

We developed the emwiki system, a Wiki service that hosts the Mizar Math-

ematics Library (MML) [4] while addressing issues with existing systems. The

emwiki system is a Web platform based on the Django framework5, featuring

4https://www.nwo.nl/en/projects/612066825

5https://www.djangoproject.com/

arXiv:2210.02336v1 [cs.PL] 21 Sep 2022

2 H. Furushima et al.

extensibility and interoperability. Vue.js6is used as the front-end framework,

making it a partial single-page application. This eliminates extra rendering to

reduce user stress. Vuetify7is used as the user interface library, which allows for

intuitive operation. Currently, this service is available at https://em1.cs.shinshu-

u.ac.jp/emwiki/release/.

2 Wiki Function

The Wiki feature is implemented to embed additional comments to read and un-

derstand articles in the MML. Although users cannot edit mathematical state-

ments written in the formal language itself, they can add comments to theorems

and deﬁnitions. We reused the HTMLized MML [18] to improve the convenience

of the MML. The HTMLized MML is a document in which the MML is converted

to HTML format, and the reference relationships are expressed as hyperlinks.

We adopted the LaTeX syntax for mathematical expressions in the comments,

which is familiar to mathematicians. MathJax [7] is used as a mathematical ex-

pression rendering engine. A real-time preview feature is also implemented to

check rendering results while editing.

The version tracking feature manages the history of comments. This function

is achieved by using Git, a distributed version control system, as its backend.

Moreover, it is necessary to maintain the linkage between theorems/deﬁnitions

and comments during library updates. Our system exploits the Git merge func-

tion for this purpose. As theorems/deﬁnitions do not have persistent identiﬁers

in the Mizar language, the most eﬀective way to identify theorems/deﬁnitions

before and after a library update is to track text diﬀerences. Our system em-

beds comments directly into the MML. Since the comments are written just

before the theorems/deﬁnitions, administrators can maintain the consistency of

the linkage between the theorems/deﬁnitions and comments using the three-way

merge function during library updates.

The user management function allows administrators to track and block ma-

licious users. The Wiki function stores a history of editors and their revisions,

and when a comment is accidentally rewritten, it is possible to contact the user

who wrote it and roll back it. Also, if a malicious comment is found, it will

be deleted, and the user who wrote it will be blocked. The user management

function is available in any component on our platform.

The screenshot of the Wiki feature is shown in Fig. 1.

3 Search Function

The emwiki system has three types of search components. The two incremental

search components accept the name of articles and symbols as input. As of 2018,

the MML contains 1,290 articles and 8,852 symbols [4], and being able to search

6https://vuejs.org/

7https://vuetifyjs.com/

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

AnIntegratedWebPlatformfortheMizarMathematicalLibraryHideharuFurushima1,DaichiYamamichi1,SeigoShigenaka1,KazuhisaNakasho1;3[0000000311104342],andKatsumiWasaki21YamaguchiUniversity,Yamaguchi,Japanfb089vgv,a102vgu,a085vgu,nakashog@yamaguchi-u.ac.jp2ShinshuUniversity,Nagano,Japanfwasakig@cs.shinshu-u.a...

展开>> 收起<<

An Integrated Web Platform for the Mizar Mathematical Library Hideharu Furushima1 Daichi Yamamichi1 Seigo Shigenaka1 Kazuhisa.pdf

共6页,预览2页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

An Integrated Web Platform for the Mizar Mathematical Library Hideharu Furushima1 Daichi Yamamichi1 Seigo Shigenaka1 Kazuhisa

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: