Datasets

1.3M+ permissively licensed theorem statements extracted from arXiv and seven mathematical sources, with slogans generated by DeepSeek V3 and Qwen3-Embedding-8B vectors.

1.2M+ subset of theorem-search-dataset, strictly covering sources with open or CC-compatible licensing. Suitable for commercial use.

Unified statement-level dependency graph: 11.7M informal arXiv statements with 18.3M dependency edges, and 388k formal Lean declarations with 11.3M typed edges across six semantic categories.

47,952 GPT-5.4-affirmed matches linking informal arXiv statements to their formal Lean counterparts, all above a 0.8 cosine similarity floor.