references.bib

% ============================================
% Knowledge Representation
% ============================================

@article{Spivak2012,
  author  = {David I. Spivak and Robert E. Kent},
  title   = {Ologs: A Categorical Framework for Knowledge Representation},
  journal = {PLoS ONE},
  volume  = {7},
  number  = {1},
  pages   = {e24274},
  year    = {2012},
  doi     = {10.1371/journal.pone.0024274}
}

@inproceedings{HyperGraphDB,
  author    = {Iordanov, Borislav},
  title     = {HyperGraphDB: A Generalized Graph Database},
  booktitle = {Web-Age Information Management (WAIM 2010 Workshops)},
  series    = {LNCS},
  volume    = {6185},
  pages     = {25--36},
  publisher = {Springer},
  year      = {2010}
}

% ============================================
% Content-Addressable Systems
% ============================================

@misc{IPLD,
  author = {{Protocol Labs}},
  title  = {IPLD --- InterPlanetary Linked Data},
  url    = {https://ipld.io},
  year   = {2021}
}

@misc{Severini2026,
  author = {Simone Severini},
  title  = {Infrastructure for Mathematics},
  year   = {2026},
  note   = {Blog post, April 2026}
}

@misc{HashMath,
  author = {Samuel Schlesinger},
  title  = {HashMath},
  year   = {2026},
  url    = {https://github.com/SamuelSchlesinger/hashmath}
}

@misc{CARepo,
  author = {Marcello Paris and Xinze Li},
  title  = {{CA} Repository},
  year   = {2026},
  url    = {https://github.com/marcellop71/CA}
}

% ============================================
% Proof Hypergraphs
% ============================================

@article{BDF2026,
  author  = {Maissam Barkeshli and Michael R. Douglas and Michael H. Freedman},
  title   = {Artificial intelligence and the structure of mathematics},
  journal = {arXiv preprint arXiv:2604.06107},
  year    = {2026}
}

% ============================================
% Coq Tools
% ============================================

@misc{CoqSerAPI,
  author = {Gallego Arias, Emilio Jes{\'u}s},
  title  = {{SerAPI}: Machine-Friendly, Data-Centric Serialization for {Coq}},
  year   = {2016},
  url    = {https://github.com/ejgallego/coq-serapi}
}

% ============================================
% Geometry and Curvature
% ============================================

@article{BLMS87,
  author  = {Bombelli, Luca and Lee, Joohan and Meyer, David and Sorkin, Rafael D.},
  title   = {Space-time as a causal set},
  journal = {Physical Review Letters},
  volume  = {59},
  number  = {5},
  pages   = {521--524},
  year    = {1987}
}

@article{Ollivier2009,
  author  = {Ollivier, Yann},
  title   = {Ricci curvature of {M}arkov chains on metric spaces},
  journal = {Journal of Functional Analysis},
  volume  = {256},
  number  = {3},
  pages   = {810--864},
  year    = {2009}
}

% ============================================
% Zero-Knowledge Proofs
% ============================================

@misc{SP1,
  author = {{Succinct Labs}},
  title  = {{SP1} --- A performant, 100\% open-source, general-purpose {zkVM}},
  year   = {2026},
  url    = {https://docs.succinct.xyz}
}

@misc{Arg23,
  author = {{Argument Computer}},
  title  = {Yatima: A zero-knowledge {Lean 4} compiler and kernel},
  year   = {2023},
  url    = {https://github.com/argumentcomputer/yatima},
  note   = {Project discontinued}
}

% ============================================
% Mathematical Formalization
% ============================================

@article{Aksenov2026,
  author  = {Vitaly Aksenov and Elena Bodnia and Michael H. Freedman and Michael Mulligan},
  title   = {Compression is all you need: Modeling Mathematics},
  journal = {arXiv preprint arXiv:2603.20396},
  year    = {2026}
}

@article{Lipkus1999,
  author  = {Alan H. Lipkus},
  title   = {A proof of the triangle inequality for the {Tanimoto} distance},
  journal = {Journal of Mathematical Chemistry},
  volume  = {26},
  pages   = {263--265},
  year    = {1999}
}

@unpublished{LPSS26b,
  author = {Xinze Li and Nanyun Peng and Patrick Shafto and Simone Severini},
  title  = {The Multinetwork of {Mathlib}: Structure, Data, and Analysis},
  year   = {2026},
  note   = {In preparation}
}

@article{LPSS26,
  author = {Xinze Li and Marcello Paris and Samuel Schlesinger and Simone Severini},
  title  = {Content-Addressing Formal Mathematics},
  year   = {2026}
}

@article{Li26,
  author = {Xinze Li},
  title  = {Astrolabe: A Content-Addressable Hypergraph for Semantic Knowledge Management},
  year   = {2026},
  note   = {arXiv preprint}
}

@misc{lean4lean,
  author = {Mario Carneiro},
  title  = {lean4lean: Lean 4 kernel reimplementation in Lean 4},
  year   = {2024},
  url    = {https://github.com/digama0/lean4lean},
}

@inproceedings{zkPi,
  author    = {Evan Laufer and Alex Ozdemir and Dan Boneh},
  title     = {zkPi: Proving Lean Theorems in Zero-Knowledge},
  booktitle = {ACM CCS},
  year      = {2024},
}