# Proofs and Essays Are Paths: An LLM ↔ Prover Loop for Falsifying Hallucinations

DevFeed: [Proofs and Essays Are Paths: An LLM ↔ Prover Loop for Falsifying Hallucinations](<https://devfeed.tech/articles/proofs-and-essays-are-paths-an-llm-prover-loop-for-falsifying-hallucinations-40135.md>)

Original publisher: [Read original article](<https://korbonits.com/blog/2026-04-30-proofs-and-essays-are-paths/>)

Published: 2026-04-30T00:00:00Z

Content type: opinion

Language: en

Sources: [Alex Korbonits](<https://devfeed.tech/sources/alex-korbonits.md>)

Topics: [Large Language Model](<https://devfeed.tech/topics/llm.md>), [Automated reasoning](<https://devfeed.tech/topics/automated-reasoning.md>), [Graphs](<https://devfeed.tech/topics/graphs.md>), [Artificial Intelligence](<https://devfeed.tech/topics/ai.md>), [Math and Logic](<https://devfeed.tech/topics/math-and-logic.md>)

Tags: [grounding](<https://devfeed.tech/tags/grounding.md>), [hallucinations](<https://devfeed.tech/tags/hallucinations.md>), [knowledge-graph](<https://devfeed.tech/tags/knowledge-graph.md>), [llm](<https://devfeed.tech/tags/llm.md>), [reasoning](<https://devfeed.tech/tags/reasoning.md>), [smt](<https://devfeed.tech/tags/smt.md>), [verification](<https://devfeed.tech/tags/verification.md>), [verify](<https://devfeed.tech/tags/verify.md>)

## AI overview

This essay proposes a bidirectional loop between a large language model and a theorem prover. LLM outputs become propositions and graph connections that the prover checks, while verification results feed back into the model. In this framework, hallucinations appear as knowledge-graph paths with edges that fail formal verification.

## Source excerpt

If a proof is a path through a formal space and an essay is a path through a semantic one, can we close the loop -- translate LLM outputs into a theorem prover, build a knowledge graph of verifiable propositions, and use the gaps as a signal for hallucination? Notebook ideas from March 2024 expanding on the SMT-grounding piece.