8 problems

A Robbins algebra is an algebra satisfying the Robbins identities. Robbins algebra conjecture. Every Robbins algebra is a Boolean algebra. McCune proved this conjecture using the E…

AI proof assistance refers to AI systems that help mathematicians develop and verify formal proofs, potentially by interacting with an interactive theorem prover. Formalization bot…

An adversarial process is a process in which AI-generated mathematical arguments are checked by an independent formal mechanism, such as an interactive theorem prover. Interactive…

Large language models (LLMs) are systems trained to generate text from natural-language data. Natural-language reasoning conjecture. Large language models (LLMs) trained on natural…

Let $T_{1}$ be the base theory for list concatenation. For a finite sequence of pairwise distinct list variables $\vec{X}=(X_{1},\dots,X_{m})$ and a sequence of non-zero natural nu…

Let $T_{1}$ be the base theory for list concatenation, and let $\mathrm{Open}(\mathcal{L}_{1})$ denote the set of open formulas in its language. Let…

Let $E$ denote a logic-based engineering application. The preceding strategy uses self-justifying axiom systems that include finitely many formally true $\Pi_1^*$ sentences and ker…

The paper considers the contrast between positive and negative results about self-justifying axiom systems and theorem provers. Conjecture on sophisticated theorem provers. Sophist…