公理化数学
公理化数学要求所有的数学都有明确的定义。
数学即代码
代码是信息的流水线。
LEAN、MathLib与数学地图
MathLib 是使用形式化证明语言LEAN记录的基础数学定理的代码库。通过mathlib的数据可视化，即代码的import关系，可得到可视化地图。
Axiomatized Mathematics
Axiomatized mathematics demands that all mathematics have precise definitions.
Mathematics as Code
Code is a pipeline for information.
LEAN, MathLib, and Mathematical Maps
MathLib is a code repository that records fundamental mathematical theorems using the formal proof language LEAN. By visualizing the data in MathLib, which represents the import relationships of the code, we can obtain a visual map.