CITATION.cff

cff-version: 1.2.0
message: "If you use ProofAtlas in research, please cite it as below."
title: "ProofAtlas: a hypergraph-metric atlas for Lean 4 proofs"
abstract: >-
  ProofAtlas is a Lean 4 library that extracts hypergraph metrics
  from formal proofs and computes their large-scale geometry. It
  provides a verified IsHypergraphMetric framework, a compute-layer
  pipeline (incidence, resistance, Gromov δ-hyperbolicity), an
  interactive #atlas.* command suite, and an executable export
  binary.
type: software
license: Apache-2.0
repository-code: "https://github.com/MathNetwork/ProofAtlas"
url: "https://proof-atlas.vercel.app"
authors:
  - family-names: Li
    given-names: Xinze
    email: lixinze0401@gmail.com
keywords:
  - lean4
  - mathlib
  - formal-mathematics
  - hypergraph
  - metric-geometry
  - proof-assistant