What question did this study set out to answer?

To create an AI agent that assists in answering logical questions reliably through dialogue and formal proofs.

March 26, 2026Open Access

Building a Logical Agent with LangChain ... and Quite Some Vibe Coding

Key Points

To create an AI agent that assists in answering logical questions reliably through dialogue and formal proofs.
Develop a logical agent using LangChain framework.
Combine a large language model with formal theorem proving.
Enable interactive dialogue for natural language to formal proof translation.
Allow inspection of both successful and unsuccessful proof attempts.
The AI effectively translates natural language questions into formal proof problems.
Users can interactively engage with the system to explore logical solutions.
The source code is partially generated using a large language model.

Abstract

This document reports on our experience of building an “agentic AI” (Artificial Intelligence) that helps a human to answer logical questions in a trustworthy way. This agent combines a Large Language Model (LLM) (which interacts with the human in natural language) with a logical software (which automatically proves formal theorems). The LLM engages in a dialogue with the human in order to translate their logical question from natural language to a formal proof problem. Once the human is satisfied with the formalization, the LLM invokes the prover to automatically solve the problem and thus answer the question; then the LLM also offers the user the possibility to inspect the successful proof or the unsuccessful proof attempt by calling the prover in an interactive mode. Furthermore, we describe how much of the source code (which is based on on the agent construction framework LangChain) has been “vibe coded”, i.e., itself generated with the help of an LLM.

Bookmark

View Full Paper