. . . . "Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving" . . . . . . . . . . . . . . . . . . . "DeepMath" . . "DeepSeek-Prover-V1.5" . . "Formal Theorem Proving by Hierarchical Decomposition" . . "GPT-f" . . "GraFormer" . . "GraphRetriever" . . "HOList" . . "HyperTree Proof Search" . . "InternLM2.5-StepProver" . . . "KG-Prover is a novel framework that uses a knowledge graph (KG) mined from mathematical texts to augment general-purpose LLMs during the inference stage for automated theorem proving. It involves iterative KG traversal for context retrieval, informal proof generation by the LLM, formal proof generation, and verification/refinement with Lean feedback. The method enhances LLM performance by providing relevant knowledge dynamically at test-time without requiring additional finetuning." . "KG-Prover" . . . "LeanDojo" . . "MUSTARD" . . "QAGNN" . . "Retrieval Augmented Generation (RAG) Baseline" . . "STP" . . "TheoremLlama" . . . "2026-02-26T15:39:09.509Z"^^ . . . "LLM-KG assessment for paper 10.48550/arXiv.2503.11657" . "RSA" . "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAwNz2QK3SEifno78S7+48zUB0xpTex3mAzW73ZimHqNcdEMU5/apslrGrTHGFAt/Chocgo++r6JQp5ygY7NyJHGWdaIqnt85pjX4PbNfLAvapyUO00qZP34fY61w4eZ9UMtleWEsmZKRtQPyJ8ODl46i/rfPuZlcJGpM9Nmy5mpGWuepqIEvF4a/t7pLVeCEDFSYXT+yaiygt6ynIK5f7TtEDhZpeUf/Q74WhMPJXm4yTU/hqOX4IW+50kWHNArGGZwUaXwzyG6M3Zd6UMModryGkLqS4H/MSE3ZA1Ylnms7BfWLEXhMWlaKi6HRV4nGRDLhxVSi9LSRi3LWKLhNIIQIDAQAB" . "BkpxW2xzAOB2r4VAvxKs3uPGHzOZ+ayqij+uaj/0T/5/qehPmAKtqG0w4kceaUJCZbnR2BQUG0lpYRvJ7t01yVteFtsBi/jj+UAuld7tzRLDiZtslXLnDDdHc4ZT2qSmO5GKE3mxwfo3+l7BvIxJ2Unz3ykzLMinTW99YNg9fSe8G2LXRWa/avs8Mlz2ybZpwKx/PWNy7uGxUP6OF4396X8rS/TMFZgfj1NaRulMGrQvrAmsROCTMKNjKiKY05/jEJa/gCwMhexG+2OlnCCdtrODtTsOiBx6TUAlXCZuZjE3QXtaunMi8iEeTQCX8DDo8gPGDNMQ0ezZSCqATDFGoQ==" . . .