Conference Program

This contribution introduces a pedagogical and methodological framework for the integration of LLMs into secondary mathematics education through logic-constrained prompt learning [1], a paradigm of structured interaction in which the prompt is conceived as a logical object and the reasoning generated by AI is explicitly constrained by formal proof procedures [2,3]. Rather than employing AI systems as solution generators, the proposed approach reconfigures them as inference-guided reasoning environments and, simultaneously, as agents of reasoning verification, whose outputs must conform to transparent deductive constraints. The framework is illustrated in the context of high-school-level Euclidean geometry problems, where the primary objective is not merely to obtain the correct result, but to master the procedural structure of mathematical inference. The central idea is to reinterpret the solution of elementary geometric problems as a satisfiability-driven logical task. The proof task is then operationalized by constructing a classical analytic tableau for the set composed of the premises together with the negation of the thesis. Closure of the tableau corresponds to the impossibility of a countermodel and therefore to the logical validity of the geometric conclusion. This transformation enables students to perceive geometric proofs not as narrative arguments, but as structured inferential processes governed by explicit rules. Within this setting, the LLM is queried under stringent procedural constraints: it must expand formulas exclusively via the standard tableau rules, label each inferential step, avoid introducing undeclared theorems, and explicitly indicate branch closures and contradictions. Such constraints reduce the model’s tendency to provide heuristic or intuitive explanations and instead impose the production of traceable proof objects. The resulting interaction introduces a form of dialogical agency, in which the AI participates in the inferential process as a regulated interlocutor, and shifts epistemic authority from the generative system to the formal framework: correctness does not depend on the plausibility of the explanation, but on the verifiability of the derivational structure. Students are thus encouraged to analyze, critique, and reconstruct the tableau, developing metacognitive awareness of proof structure and logical dependencies among statements. From a theoretical perspective, the framework establishes a constructive equivalence between elementary geometric demonstration and formal logical consequence, offering a unified view of mathematical reasoning across different domains. From a pedagogical perspective, it supports three complementary learning outcomes: explicit understanding of deductive chains in geometry, development of formalization skills through controlled propositional encoding of mathematical statements, and critical engagement with AI outputs as objects of validation rather than authoritative answers. The approach is compatible with collaborative classroom practices such as inquiry-based learning and thinking-classroom models, and requires only minimal formal knowledge beyond an introduction to classical propositional logic. The proposed methodology contributes to research on human-centered AI in education by offering a replicable model for integrating LLMs into proof-oriented disciplines without sacrificing rigor or transparency. Through the direct incorporation of formal proof procedures into the prompt structure, logic-constrained prompt learning enables AI to operate simultaneously as an environment and an agent of reasoning verification, thereby fostering reflective judgment, rigorous reasoning, and participatory learning contexts.