\section{Formulations and Frameworks}
\label{sec:fps}
Please refer to Appendix~\ref{app:background} for the background about FTP. In this section, we first present rigorous definitions of \textit{problem} and \textit{answer}, and formulate the problem-solving processes as a deterministic Markov decision process with a déjà vu to formal verification. Then, we propose \textbf{FPS} (\textit{\ul{F}ormal \ul{P}roblem-\ul{S}olving}), a framework to encompass problem-solving processes inside existing TP environments. In FPS, the resulting solutions are process-verified, and the soundness of answers is ensured. For \textit{find-all problems}, deductive solving is usually more human-readable. We further propose \textbf{D-FPS} (\textit{\ul{D}eductive \ul{FPS}}), decoupling solving and verification to enhance deductive reasoning.

\subsection{Definitions and Formulations of Problem-Solving}\label{sec:ftp:formulation}
Consider the following problems (more examples and formalizations are in Appendix~\ref{sec:exemplar_formalizations:example}):
\begin{enumerate}[leftmargin=10pt, topsep=0pt,itemsep=1pt,partopsep=1pt, parsep=1pt]
  \item \textit{Yes-no question}: Does there exist a positive real number $\alpha$ s.t. $[\alpha^n] - n$ is even for all $n \in \mathbb N^+$?
  \item \textit{Equation}: Solve $x \in \mathbb R \text{ s.t. } x^2 - 1 = 0$.
  \item \textit{Calculation}: Calculate $\lim_{n\rightarrow \infty} \frac{2}{n}$.
  \item \textit{Simplification}: Simplify $\sqrt{28x} \cdot \sqrt{15x} \cdot \sqrt{21x}$.
  \item \textit{Counter-example construction}: Find a Fermat number $F_n = 2^{2^n} + 1$ which is not prime.
\end{enumerate}
All of them consist of variables (including a queried variable), hypotheses, and conclusions that the answer must satisfy. More generally, all \textit{elementary questions} (\textit{whether-questions} and \textit{which-questions})~\cite{belnap1976logic} can be expressed in this form~\cite{nickles1981problem}. Their answers are terms (e.g., numbers and functions) that depend on variables defined before the queried variable. Formally,

\begin{definition}\label{def:problem}
A \textit{\textbf{problem}} $P(\hat a) = (\forall_{i=1}^n v_i, \bigwedge_{i=1}^p\phi_i \rightarrow \bigwedge_{i=1}^q\psi_i)[a\mapsto \hat a]$ is a predicate\footnote{$\phi[x \mapsto t]$ represents substituting a term $t$ for a variable $x$ in a formula $\phi$ at the places where $x$ occurs free.} that maps a direct answer $\hat a$ to a proposition. $P$ is composed of $(V, a, \Phi, \Psi)$, where
\end{definition}
\begin{itemize}[leftmargin=10pt, topsep=0pt,itemsep=1pt,partopsep=1pt, parsep=1pt]
  \item \textit{Independent variables} $V=\{v_i\}_{i=1}^n$ is the set of variables independent to $a$;
  \item \textit{Queriable}\footnote{We follow the terminology in \cite{belnap1976logic}, although our formulations differs.} $a$ is the queried variable that occurs free in $\forall_{i=1}^n v_i, \bigwedge_{i=1}^p\phi_i \rightarrow \bigwedge_{i=1}^q\psi_i$;
  \item \textit{Hypotheses} $\Phi = \{\phi_i\}_{i=1}^p$ is the set of propositions that depend on $V$ (whose all free variables are included in $V$), consisting of conditions that can be used to deduce the answer.
  \item \textit{Conclusions} $\Psi = \{\psi_i\}_{i=1}^q$ is the set of propositions which depend on $V \cup \{a\}$, consisting of conclusions that should be satisfied.
\end{itemize}

\begin{definition}\label{def:direct_answer}
A \textit{\textbf{direct answer}} is a term $\hat a$ which depends on $V$.
\end{definition}

To avoid vacuous discussions of insolvable problems and following \cite{belnap1976logic}, we presuppose the problems under discussion to be satisfiable.

\begin{assumption}\label{ass:satisfiable}
A problem is presupposed to be \textbf{\textit{satisfiable}}, i.e., the following propositions hold.
  \begin{equation}\label{eq:satisfiable}
  \forall_{i=1}^n v_i, \bigwedge_{i=1}^p \phi_i \rightarrow \exists a, \bigwedge_{i=1}^q \psi_i
  \end{equation}
\end{assumption}

``Solving a problem'' is essentially delineating two requirements: \textbf{1) Finding a direct answer $\hat a$}; \textbf{2) Proving $P(\hat a)$}.  A step-by-step solution simultaneously finds a valid $\hat a$ and constructs a proof of $P(\hat a)$. The queriable $a$ is treated as a ``hole'', which serves as a free variable and is finally filled with a direct answer $\hat a$. In a non-aftereffect manner, solution steps manipulate solution states, which consist of all known conditions, target conclusions, and existing holes. When all holes are filled, and all target conclusions are satisfied, the problem is successfully solved. Detailed discussions of reasoning patterns in solution steps can be found in Appendix~\ref{app:exemplar_reasoning_patterns}. In this view, the problem-solving process can be modeled as a deterministic MDP $(\mathcal S, \mathcal A, P, R)$.

\begin{definition}\label{def:solution_state}
A \textit{\textbf{solution state}} $S = (H, G) \in \mathcal S$ maintains unfilled holes and unproven goals.
\end{definition}
\begin{itemize}[leftmargin=10pt, topsep=0pt,itemsep=1pt,partopsep=1pt, parsep=1pt]
  \item $H$ is the set of unfilled \textit{holes}, $H = \{(?h_i, V_i, \Phi_i)\}_{i=1}^s$, where $?h_i$ is the placeholder of the $i$-th hole, $V_i = \{v_{i,j}\}_{j=1}^{n_i}$ is a set of variables, $\Phi_i = \{\phi_{i,j}\}_{j=1}^{p_i}$ is a set of hypotheses which depend on $V$ and other holes. Notice that circular dependency of holes is not allowed.
  \item $G$ is the set of unproven \textit{goals}, $G = \{(V_i, \Phi_i, \Psi_i)\}_{i=1}^r$, where $V_i = \{v_{i,j}\}_{j=1}^{n_i}$ is a set of variables, $\Phi_i = \{\phi_{i,j}\}_{j=1}^{p_i}$ is a set of hypotheses dependent on $V$ and $H$, and $\Psi_i = \{\psi_{i,j}\}_{j=1}^{q_i}$ is a set of conclusions dependent on $V$ and $H$. Each goal represents one proposition $P_i=\forall_{j=1}^{n_i} v_{i, j}, \bigwedge_{j=1}^{p_i}\phi_{i, j} \rightarrow \bigwedge_{j=1}^{q_i}\psi_{i, j}$ should be proven.
\end{itemize}

\begin{definition}\label{def:solution_step}
A \textit{\textbf{solution step}} $s\in \mathcal A$ is a function $s : (H, G) \mapsto (H^\prime, G^\prime)$ that maps a solution state $(H, G)$ to $(H^\prime, G^\prime)$ by manipulating holes and goals.
\end{definition}

Given a problem with $(V, a, \Phi, \Psi)$, the initial solution state is $(\{?a, V, \Phi\}, \{V, \Phi, \Psi[a\mapsto ?a]\})$. By sequentially executing solution steps $s_i$ in \textit{\textbf{solution}} $\boldsymbol s = [s_i]_{i=1}^m$, the initial solution state is finally transformed to the \textit{terminal state} $(\{\}, \{\})$, where all holes are filled and all goals are proven, i.e. $(\{\}, \{\}) = (s_m \circ s_{m-1} \circ \dots \circ s_1)((\{?a, V, \Phi\}, \{V, \Phi, \Psi\}))$. A problem-solving agent can be rewarded if the solution is successfully constructed, i.e., $R_s(S, S^\prime) = \mathbb{I}_{S^\prime = (\{\}, \{\})}$.




\begin{figure*}[t!]
  \centering
  \includegraphics[width=\linewidth]{figs.FPS_MDP.pdf}
  \caption{Demonstrations of FPS and D-FPS. FPS: After initialization, an agent iteratively executes solution steps to transform solution states until all goals are solved. A direct answer and its soundness proof can be extracted. D-FPS: The whole process is further decoupled into a forward-solving part and an optional backward-proving part. Forward-solving enforces deductive reasoning for better human readability. The direct answer and the completeness proof can be extracted upon finishing forward-solving, while the soundness proof should be extracted after finishing backward-proving.}
  \label{fig:fps_dfps}
  \vspace{-15pt}
\end{figure*}

\vspace{-2pt}
\subsection{Formal Problem-Solving Framework}\label{sec:fps def}
Readers familiar with formal theorem proving may feel an intense déjà vu: both theorem proving and problem-solving can be modeled as a deterministic MDP, both proof states and solution states consist of goals to prove and holes to fill, and both tactic applications and solution steps transform the states towards the terminal state. Based on these parallels, we implement the problem-solving processes in the FTP environment Lean 4 for its maturity and popularity. Similar implementations are also available in other environments, e.g., Coq, where more convenient \texttt{eexists} and \texttt{evar} can be used.

\noindent\textbf{Problems.} The theory foundation of Lean 4 is dependent type theory~\cite{theorem_proving_in_lean4}. Therefore, for problem $(V, a, \Phi, \Psi)$, $P$ should be rewritten in Lean 4 as 
$$P(\hat a) = (\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), (\wedge_{i=1}^q \psi_i))[a \mapsto \hat a]$$
Prop.~\ref{eq:satisfiable} should be rewritten as
\begin{equation}\label{eq:satisfiable_dtt}
  \forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \exists (a : T_a), \wedge_{i=1}^q\psi_i
\end{equation}
where $T_i$ is the type of the independent variable $v_i$, $T_a$ is the type of the queriable $a$, and dependent type notations are omitted for brevity.

\noindent\textbf{Problem-Solving.} Sec.~\ref{sec:ftp:formulation} concludes the essence of problem-solving as finding a direct answer $\hat a$ and a proof for $P(\hat a)$. These two targets can be further summarized as finding a constructive proof (w.r.t $a$) of Prop.~\ref{eq:satisfiable_dtt}. 
We name this framework as \textbf{FPS} (\textit{\ul{F}ormal \ul{P}roblem-\ul{S}olving}) in line with formal theorem proving (FTP). A demo is in Fig.~\ref{fig:fps_dfps} (left), where
\begin{itemize}[leftmargin=10pt, topsep=0pt,itemsep=1pt,partopsep=1pt, parsep=1pt]
    \item \textbf{Initialization.} The Lean 4 environment is initialized with Prop.~\ref{eq:satisfiable_dtt}. Then, variables in $V$ and hypotheses in $\Phi$ are introduced. The queriable $a$ is split as a metavariable \texttt{?w} by \texttt{apply Exists.intro}. \texttt{?w} is coupled~\cite{limperg2023aesop,aniva2024pantograph} with the main goal \texttt{h} to prevent non-constructive proofs\footnote{The logical foundation of Lean, calculus of construction, follows intuitionistic logic and rejects non-constructive axioms, e.g., the axiom of choice and the law of excluded middle. However, Lean assumes the axiom of choice (and subsequently admits the law of excluded middle) to facilitate proving.} and facilitate answer extraction while maintaining semantics. Lean code and generic initial proof states are in Appendix~\ref{app:FPS}. The resulting initial solution state is \texttt{State 0}.
    \item \textbf{Solving.} The solution states and solution steps are implemented as proof states and tactic applications in Lean 4. To solve a problem, starting from \texttt{State 0}, an agent iteratively interacts with Lean 4, manipulating the solution states. The terminal state \texttt{State m} consists of no unsolved goals. Once the agent finds a sequence of tactics $\boldsymbol s = [s_i]_{i=1}^m$ which transforms \texttt{State 0} to \texttt{State m}, the problem is successfully solved with the formal solution $\boldsymbol s$.
    \item \textbf{Extraction.} Once the problem-solving succeeds, we extract the direct answer $\hat a$ from the metavariable assignments in Lean kernel.
\end{itemize}

\begin{theorem}\label{def:soundness_fps} \textup{(Proof in Appendix~\ref{app:proof:soundness_fps})}
FPS is \textbf{sound}: for any problem $P$ and direct answer $\hat a$ resulted from FPS, $P(\hat a)$ holds.
\end{theorem}

\noindent\textbf{Discussion.} There are two main types of problems. \textit{Find-one problems} are problems requiring one valid answer, e.g., counter-example construction. \textit{Find-all problems} require finding all valid answers (unique one or multiple candidates), e.g., equation solving and computation. For find-all problems, FPS does not need a ``completeness theorem'' but ensures that all answers are found by proper formalization. For example, a multiple-answer problem with ground-truth answer set $\bar a$ can be formalized as
$(V, (a : \texttt{Set}\ T_x), \Phi, \{a = \{x : T_x | \bigwedge_{i=1}^q \psi_i\}\})$
or
$(V \cup \{(x : T_x)\}, (a : \texttt{Set}\ T_x), \Phi, \{\bigwedge_{i=1}^q \psi_i \leftrightarrow x\in a\})$
(neither $a$ nor $x$ occurs free in $\Phi$).

The intense affinity between FPS and FTP is a double-edged sword. It allows direct application of existing FTP methods without fine-tuning. However, it inherits the flexibility from FTP, which allows mixed forward-backward reasoning and the ``guess-then-check'' paradigm. For find-one problems, this framework works well. For find-all problems, humans usually prefer deductive and declarative reasoning processes~\cite{sep-reasoning-automated,ahuja2025improver,10.1007/978-3-642-14052-5_9}.


\vspace{-5pt}
\subsection{Deductive Formal Problem-Solving Framework}
\vspace{-5pt}
\label{sec:dfps}
To force deductive solving for find-all problems, we focus on a ``subset'' of FPS, namely \textbf{D-FPS} (\textit{\ul{D}eductive \ul{FPS}}), whose problems should satisfy:
\begin{itemize}[leftmargin=10pt, topsep=0pt,itemsep=1pt,partopsep=1pt, parsep=1pt]
\item The queriable $A$ lives in the universe of propositions, i.e., $A : \texttt{Prop}$;
\item $\Psi = \{\psi \leftrightarrow A\}$ and $\psi$ only depends on $V$, i.e., $A$ doesn't occur free in $\psi$.
\end{itemize}

\begin{theorem}\label{def:expressiveness_dfps}
\textup{(Proof in Appendix~\ref{app:proof:expressiveness_dfps})} 
Regarding find-all problems, the expressiveness of D-FPS is at least as strong as that of FPS.
\end{theorem}

A demo of D-FPS is in Fig.~\ref{fig:fps_dfps} (right), where
\begin{itemize}[leftmargin=10pt, topsep=0pt,itemsep=1pt,partopsep=1pt, parsep=1pt]
    \item \textbf{Initialization.} The proof state is initialized as in FPS. Then, the main goal \texttt{h} is explicitly split into a forward goal \texttt{h.mp} and a backward goal \texttt{h.mpr} with corresponding hypotheses introduced. We use \textit{forward state} to refer to the goal \texttt{h.mp} and the hole \texttt{?w} (usually omitted for brevity), and \textit{backward state} to refer to the goal \texttt{h.mpr}. Code implementation and generic initial proof states are in Appendix~\ref{app:DFPS}. The initial forward state is \texttt{Forward State 0}, and the initial backward state is \texttt{Backward State 0}.
    \item \textbf{Solving.} The problem-solving process is explicitly split into a forward-solving part and a backward-proving part. A problem-solving agent uses deductive reasoning to derive new conclusions in forward reasoning iteratively. If the agent simultaneously\footnote{Otherwise, after \texttt{?w} is filled by $\hat A$, the target of the forward state is concretized as $\hat A$. Hence, tactics of backward reasoning can be applied to  this goal.} fills \texttt{?w} and proves \texttt{h.mp} by a simple \texttt{exact} tactic, the forward-solving is finished. Then, it can early-exit or continue to finish the backward-proving part, i.e., proving \texttt{h.mpr}.
    \item \textbf{Extraction.} Once forward-solving succeeds, we extract the direct answer $\hat A$ from the metavariable assignments in Lean kernel.
\end{itemize}



\begin{theorem}\label{def:completeness_dfps}
\textup{(Proof in Appendix~\ref{app:proof:completeness_dfps})} 
D-FPS is \textbf{complete}: for any find-all problem with ground-truth $\bar A$, for any direct answer $\hat A$ resulted from D-FPS, the following assertion holds: $$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \bar A \rightarrow \hat A$$
\end{theorem}

\begin{theorem}\label{def:soundness_dfps}
\textup{(Proof in Appendix~\ref{app:proof:soundness_dfps})} D-FPS is \textbf{sound}: for any find-all problem with ground-truth $\bar A$, for any direct answer $\hat A$ resulted from D-FPS, if the backward-proving is finished, it holds: $$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \hat A \rightarrow \bar A$$ 
\end{theorem}