arXiv subjects

Artemii Remizov

Publications and source records attributed to Artemii Remizov.

3 recordsLinked to original sources

arXiv2026

TheoremGraph: Bridging Formal and Informal Mathematics

Mathematical knowledge is organized around statements and their dependencies, but this structure is exposed unevenly: informal papers cite mostly at the document level, while formal libraries record fine-grained dependencies over a much smaller body of mathematics. We introduce TheoremGraph, a unified statement-level dependency graph spanning both informal and formal mathematics. On the informal side, we parse 11.7M theorem-like environments from mathematics arXiv and recover 18.3M candidate directed dependencies, each labeled by the extractor that proposed it so downstream users can trade coverage for precision. On the formal side, we release LeanGraph, a Lean 4 elaborator-level extractor producing 388,105 declaration nodes and 11.3M typed edges across 25 Lean projects. We bridge the two graphs by embedding generated natural-language slogans into a shared semantic space, linking related statements across papers and across the informal/formal divide; an LLM judge affirms 47,952 such matches above a 0.8 cosine floor, with the judge-acceptance rate rising from 48% across the floor to 87% in the >=0.9 tier. On formal concept retrieval, our name-and-signature representation with graph expansion comes within 0.5pp of LeanSearch v2's reranked Recall@10 (0.775 vs. 0.780) without an LM reranker. We release the dataset, extractors, HTTP API, and MCP interface as infrastructure for mathematical search, attribution, and retrieval-augmented reasoning, available at theoremsearch.com and huggingface.co/datasets/uw-math-ai/theorem-matching.

cs.IR↗

arXiv2026

Semantic Search over 9 Million Mathematical Theorems

Searching for mathematical results remains difficult: most existing tools retrieve entire papers, while mathematicians and theorem-proving agents often seek a specific theorem, lemma, or proposition that answers a query. While semantic search has seen rapid progress, its behavior on large, highly technical corpora such as research-level mathematical theorems remains poorly understood. In this work, we introduce and study semantic theorem retrieval at scale over a unified corpus of $9.2$ million theorem statements extracted from arXiv and seven other sources, representing the largest publicly available corpus of human-authored, research-level theorems. We represent each theorem with a short natural-language description as a retrieval representation and systematically analyze how representation context, language model choice, embedding model, and prompting strategy affect retrieval quality. On a curated evaluation set of theorem-search queries written by professional mathematicians, our approach substantially improves both theorem-level and paper-level retrieval compared to existing baselines, demonstrating that semantic theorem search is feasible and effective at web scale. The project page, search tool, dataset, REST API, and MCP server are available at theoremsearch.com.

cs.IR↗

arXiv2025

Quantifying the Hemodynamic Effects of Ventricular Fibrillation using a Verified Computational Model

Ventricular Fibrillation (VF) is a malignant cardiac arrhythmia and the leading cause of sudden cardiac death, characterized by disorganized, high-frequency ventricular activity that results in the rapid loss of coordinated pump function and circulatory collapse. While the clinical manifestations of VF are well established, the multiscale mechanisms linking cellular electrophysiology to whole-organ mechanical failure remain challenging to study experimentally. Computational modeling therefore provides a critical platform for mechanistic investigation. This work presents a hierarchical computational study of VF beginning with the implementation and verification of a closed-loop, lumped-parameter (0D) hemodynamic model of the cardiovascular system. The verified model is used to quantify the global circulatory consequences of a prescribed VF state, demonstrating a 62.4% reduction in cardiac output and highlighting the dominant role of impaired ventricular filling and contractile failure. Recognizing the limitations of prescribing arrhythmia dynamics, we then propose a pathway toward an integrated, multiscale framework coupling the 0D hemodynamic core with models of cardiac electrophysiology and autonomic regulation to enable simulation of emergent arrhythmogenic behavior and reflex responses. Finally, we introduce an interactive simulator derived from the verified 0D model, designed to support education, hypothesis testing, and future integration of multiscale components. This work establishes a mechanistic baseline and software foundation for next-generation computational studies of VF and cardiovascular control.

physics.bio-ph↗