Greetings

[ducourtial.metam...@passfwd.com]

Dear Metamath community,

My name is Adrian Ducourtial, and I would be interested in contributing to the Metamath project, primarily the set.mm database. As is recommended, I will be starting slow and learning the language from there. In any case, I find the clear and principled approach to mathematical theory, at the core of Metamath's philosophy, to be valuable and worthwhile.

As a first, superficial contribution, I have spotted a typo in the description of the theorem 4on: It should begin "Ordinal 4..." rather than "Ordinal 3...". I'm still learning the whole GitHub flow, however.

PS. As this mailing list is public, I have chosen to subscribe with a forwarding email address. My GitHub account is @ducourtial.

Best wishes,
Adrian

[Jim Kingdon]

On 3/17/25 11:47, ducourtial.metamath.monologue534 via Metamath wrote:

My name is Adrian Ducourtial, and I would be interested in contributing to the Metamath project

Welcome.

As a first, superficial contribution, I have spotted a typo in the description of the theorem 4on: It should begin "Ordinal 4..." rather than "Ordinal 3...". I'm still learning the whole GitHub flow, however.

Good catch.

Hopefully it isn't too hard to learn how to submit this change via github - I realize it isn't exactly mathematical learning but it is central enough to this project (and some other mathematical projects too) that submitting this change via github should be a nice way to get to know the process.

[ducourtial.metam...@passfwd.com]

Hopefully it isn't too hard to learn how to submit this change via github

I have attempted a pull request fixing the typo—hope it's visible.

[Glauco]

Hi Adrien,

Welcome to the Metamath community! It’s great to have you here.

I noticed that your pull request didn’t pass the initial checks, specifically due to text rewrapping issues. Don’t worry—this is a common hurdle when starting out, and the set.mm maintainers are always happy to guide you through the process. They’ll likely provide feedback on your PR soon.

Before submitting a pull request, it’s helpful to follow the formatting recommendations outlined in the CONTRIBUTING.md guidelines. These ensure your changes align with the project’s standards.

If you have any questions or need assistance, feel free to ask. We’re here to help! Looking forward to seeing your contributions.

Best,

Glauco

[Glauco]

Hi Adrien,

Hi Adrian,

(sorry, for misspelling)

[ducourtial.metam...@passfwd.com]

(sorry, for misspelling)

No worries, thank you for the inviting message! I'll make sure to use the `rewrap` command going forward.