Morley theorem

[jagra]

Hi all,

I have produced a formalization of Morley, based on Alain Connes proof, heavily supported by LLMs (Claude and Codex), available at https://github.com/jorge-agra/morley-metamath

I have recently submitted a formalization of triangle congruence as a set.mm contribution, also supported by LLMs, that was quite large and took some time to be reviewed and merged (today, thank you to all reviewers for their patience and good will), and feel that, maybe, this type of contributions should stay out of main set.mm. Though about retiring it a few times, not because it was taking its time, but because I felt the burden that review caused you. So sorry for that.

Don't want to call my formalization's AI math slop, but guess they kind of are. I am an engineer/sw architect and am more interested in the proof construction process than on the proofs themselves. And probably, metamath community is on the opposite side, so reviewing AI generated proofs is not an interesting activity for you.

At a completely different scale, a similar problem that global math community is having with recent OpenAI proofs.

Nevertheless, I believe that metamath is an excellent target for formalization with LLMs and provides a bridge between informal and formal with much less friction to LLMs than programming languages.

Of course, for this to work, an architecture and process around contributions must be built so that my and future contributions can be integrated without pain.

Thank you all to keep it going all this years. Lean is great but not as fun as metamath.

Best regards,

Jorge Agra

[Jim Kingdon]

Thank you for your patience on that triangle congruence pull request.

As for what is best kept to people's own sites, what belongs in a mathbox, and what belongs in the main set.mm/iset.mm, not a super simple topic but we have tried to express our thoughts/rules at places like https://us.metamath.org/mpeuni/conventions.html and https://us.metamath.org/mpeuni/mathbox.html . These issues are not created by autoformalization, but autoformalization can intensify them.

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/bd47e7be-6087-4eac-9738-b3291b0caa99n%40googlegroups.com.

[Jorge Agra]

Hi,

Maybe I didnt expressed myself clearly. Not my intention to keep anything on a repo outside set.mm.

If anyone thinks that morley formalization should be submitted, great. Thats why I did it.

But would like to have some feedback on it if possible:

- Is it worth a aubmission? Not tarski ...

- In small pieces or bulk?

Best regards.

To view this discussion visit https://groups.google.com/d/msgid/metamath/CAMVL0mCfmuaS9edVHe78QZmPR3Gei-QZRu5EnyF8hciAvWjQhw%40mail.gmail.com.