btw, it use mmverify.py by default and CI, you can add other verifiers: ``` skfd verifier list skfd verfier add knife KNIFE_PATH ```
Mingli On Thu, Feb 12, 2026 at 8:43 AM Mingli Yuan <[email protected]> wrote: > Hi Glauco, > Please try again with new clones, I have updated some scripts. > > Verifying each single proof will generate the *.mm file in the target > folder. > > Verifying the whole project will generate *.mm file and source map files > in the target folder also. > > ``` > uv run --frozen skfd verify proof-lab > ``` > > Best, > > Mingli > > > On Thu, Feb 12, 2026 at 5:46 AM Glauco <[email protected]> wrote: > >> Hi Mingli, >> >> I've tried it in Play-With-Docker, here is the script that worked for me >> (from a clean new PWD instance): >> >> curl -LsSf https://astral.sh/uv/install.sh | sh >> source $HOME/.local/bin/env >> git clone https://github.com/epistemic-frontier/metamath-logic.git >> git clone https://github.com/epistemic-frontier/metamath-prelude.git >> git clone https://github.com/epistemic-frontier/proof-lab.git >> cd proof-lab >> uv run skfd verify prove_modus_tollens.py >> >> >> here's the output >> >> [node1] (local) [email protected] ~/proof-lab >> $ uv run --frozen skfd verify prove_modus_tollens.py >> Verifying script: prove_modus_tollens.py ... >> Found 1 proof(s): prove_modus_tollens >> Running prove_modus_tollens... OK (modus_tollens) >> Emitting 1 proofs to Metamath... OK >> >> Is the proof stored somewhere? >> >> Glauco >> >> >> Il giorno mercoledì 11 febbraio 2026 alle 21:32:18 UTC+1 >> [email protected] ha scritto: >> >>> 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/1dab7fa9-5e07-43f9-81d0-22c2209b1127n%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/1dab7fa9-5e07-43f9-81d0-22c2209b1127n%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/CAGDRuAjHiNzJLbuExQ9UQ2Hb5mrj9Q7bMA8fxT11WkbkNYhS_A%40mail.gmail.com.
