Hi Glauco, I saw your email and felt very inspired. So I worked late this night to make the code ready.
Now I have published metamath-prelude and metamath-logic. They are still "alpha" versions and not perfect, but I think they are usable now. *1. Proof Lab* I made a new repo called *Proof Lab* here: https://github.com/epistemic-frontier/proof-lab You can clone it and just follow the README. It can verify the Python proofs (like your mp2 example) using the real Metamath verifier. *2. Original Authorship* Also, I want to say one thing. Even though I use a Python interface, I try my best to keep the original author's comments in the source code. For example, please check this file: https://github.com/epistemic-frontier/metamath-logic/blob/main/src/logic/propositional/hilbert/lemmas.py#L222 You can see the note from *NM (Norman Megill) on 30-Sep-1992* is kept there. I think attribution is very important. Please try the lab. Let me know if you have any problems. Best, Mingli On Wed, Feb 11, 2026 at 10:33 PM Mingli Yuan <[email protected]> wrote: > Hi Glauco, > > Thanks for checking. > > Logically, the structure is correct: from φ and (φ → (ψ → χ)) we get (ψ → > χ) by MP, then from ψ we get χ by MP again. So the *proof skeleton* is > right. > > However, my porting work is not finished yet, the > logic.propositional.hilbert and related packages are not released yet, so > this code can not be verified by the community right now. There are around > 20k lines of proofs in the logic part of metamath, please give me some time > to finish it. > > Or, I may release the prelude and logic package earlier before it is fully > ported, if anyone is interested. > > Best, > > Mingli > > On Wed, Feb 11, 2026 at 9:07 PM Glauco <[email protected]> wrote: > >> Hi Mingli Yuan, >> >> I've given Gemini your README.md and asked it to prove mp2 with your >> framework. Below is the Python code that Gemini returned. >> Is it completely hallucinated, or is it close? >> >> from logic.propositional.hilbert import System >> from logic.propositional.hilbert.lemmas import Proof, ProofBuilder >> >> def prove_mp2(sys: System) -> Proof: >> """ >> Double Modus Ponens: φ, ψ, (φ → (ψ → χ)) ⊢ χ >> """ >> # 1. Initialize the builder with the system and theorem name >> lb = ProofBuilder(sys, "mp2") >> >> # 2. Define Hypotheses (mp2.1, mp2.2, mp2.3) >> h_phi = lb.hyp("mp2.1", "φ") >> h_psi = lb.hyp("mp2.2", "ψ") >> h_chi_nested = lb.hyp("mp2.3", "φ → (ψ → χ)") >> >> # 3. Apply the first Modus Ponens (Step 4 in .mmp) >> # This uses h_phi and h_chi_nested to get (ψ → χ) >> step4 = lb.mp("s1", h_phi, h_chi_nested, note="Step 4: MP h_phi, >> h_chi_nested") >> >> # 4. Apply the second Modus Ponens (Step 5 in .mmp) >> # This uses h_psi and step4 to get χ >> step5 = lb.mp("s2", h_psi, step4, note="Step 5: MP h_psi, s1") >> >> # 5. Return the build targeting the final result >> return lb.build(step5) >> >> BR >> Glauco >> >> Il giorno mercoledì 11 febbraio 2026 alle 08:05:05 UTC+1 >> [email protected] ha scritto: >> >>> Dear Metamath Community, >>> >>> I am writing to share an open-source project we have been working on >>> called ProofScaffold ( >>> https://github.com/epistemic-frontier/proof-scaffold). >>> >>> Our team has deep respect for set.mm and the rigorous foundation this >>> community has built. However, as we explore the intersection of Metamath >>> and Large Language Models (LLMs), we’ve encountered a persistent challenge: >>> feeding a 48MB monolithic file to an AI often leads to context dilution, >>> hallucinated imports, and noisy proof searches. >>> >>> To solve this, we built ProofScaffold. It acts as a package manager and >>> linker (written in Python) for Metamath. It allows us to split massive >>> databases into composable, compilable, and independently verifiable >>> packages with explicit dependencies and exports—much like Cargo or NPM, but >>> for formal math. >>> >>> Crucially, the Trust Computing Base (TCB) does not change. Python acts >>> strictly as an untrusted builder/linker. The final output is a standard, >>> flattened .mm transient monolith that is verified by metamath-exe or >>> metamath-knife. >>> >>> We believe this modularity is the key to unlocking AI's true potential >>> in formal mathematics: >>> >>> - Targeted Retrieval: By scoping the context to a specific package >>> (e.g., just fol or zf), we drastically reduce noise for the LLM. >>> >>> - Controlled Semantic Boundaries: Explicit exports provide the AI with a >>> strict subset of permissible symbols and axioms. This prevents hallucinated >>> reasoning, such as an AI accidentally employing the Axiom of Choice in a >>> strict ZF-only context. >>> >>> - Verifiable Incremental Loops: An AI can generate a proof, verify it >>> locally within the package, and map any verifier errors directly back to >>> the specific package contract (e.g., missing $f or label conflicts). This >>> makes AI self-correction much more reliable. >>> >>> - Curriculum Alignment: Modular packages naturally form a curriculum >>> (axioms → definitions → lemmas → theorems), providing high-quality gradient >>> data for training models, rather than overwhelming them with the entire >>> set.mm at once. >>> >>> We have successfully ported a prelude and are currently porting the >>> logic package (aligned with the |- conventions of set.mm). Our next >>> step is to further subdivide logic into prop, fol, eq, and setvar packages, >>> and to generate machine-readable interface manifests to help AI planners. >>> >>> A Question for the Community regarding PyPI Naming: >>> >>> To make this ecosystem easily accessible for AI researchers and >>> engineers, we plan to publish these modularized databases as Python >>> packages on PyPI. >>> >>> I would like to ask if the community is comfortable with us using the >>> metamath- prefix for these packages (e.g., metamath-logic, metamath-zfc). I >>> want to be entirely respectful of the Metamath trademark/legacy and ensure >>> this doesn't cause confusion with official tools. If the community prefers >>> we use a different namespace (e.g., proof-scaffold-logic), we will gladly >>> do so. >>> >>> I would love to hear your thoughts, feedback, or critiques on this >>> approach. >>> >>> Best regards, >>> >>> Mingli Yuan >>> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion visit >> https://groups.google.com/d/msgid/metamath/6caee51b-6405-4a23-837e-8d47339b5df7n%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/6caee51b-6405-4a23-837e-8d47339b5df7n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CAGDRuAiba7CcN3wOnT4Q0tP%3DSyXg0u9mKhFLKX4EoA7eBCE0ig%40mail.gmail.com.
