Valeria de Paiva writes that she was quoted in a new book by Simone Severini and Andrea Borghini, *Science, Ltd.: Notes on the Research Enterprise in the Age of Machines*, and reflects on the advice she gave in 2023. The central claim is that mathematical knowledge should not be reduced to formal systems alone; instead, the priority is extracting semantic meaning from natural-language texts before formalizing, because natural language is an extraordinarily successful technology that humans have developed over hundreds of thousands of years and is unlikely to be rendered obsolete by proof assistants or language models. She advocates building bridges between informal and formal mathematics through a "Network Mathematics" knowledge graph that connects concepts, theorems, papers, and formal statements across the different ways mathematics exists.
- Her project Network Mathematics aims to represent mathematical knowledge as an extended knowledge graph rather than a pile of documents or a single formal library
- MathGloss attempts to align mathematical concepts across resources written for humans and those intended for machines
- She acknowledges she underestimated the age of natural language, saying "thousands of years" when fully developed human language likely dates back at least 100,000 years
- Her project Network Mathematics aims to represent mathematical knowledge as an extended knowledge graph rather than a pile of documents or a single formal library
- MathGloss attempts to align mathematical concepts across resources written for humans and those intended for machines
- She acknowledges she underestimated the age of natural language, saying "thousands of years" when fully developed human language likely dates back at least 100,000 years
Dimension Reducers builds tools to formalize, stress-test, verify, and structure mathematical knowledge. They offer solutions for LLM training, automated refereeing, and retrieval that understands mathematical structure. Their platform includes tools for refereeing at scale, adversarial testing ("torture testing"), and structured Retrieval Augmented Generation (RAG).
Key products include DiRe-JAX (a dimensionality reduction library), arXiv Math Semantic Search, arXiv Proof Audit Database, Mathematics Torture Chamber, and a Lean 4 Formalization Pipeline. They also publish research and benchmarks in mathematical formalization and OCR, emphasizing semantic accuracy and robustness.
Key products include DiRe-JAX (a dimensionality reduction library), arXiv Math Semantic Search, arXiv Proof Audit Database, Mathematics Torture Chamber, and a Lean 4 Formalization Pipeline. They also publish research and benchmarks in mathematical formalization and OCR, emphasizing semantic accuracy and robustness.
