Formalizing Mathematics in LEAN

Dear participants,

Here are some details for the submission next week.

Remember: The Deadline is end of day next Sunday, 15th March, 23:59:59. All changes made after this point will not be considered for the grading. This includes your code as well as the documentation.

To mark your submission, please tag your submission in your repository. The tag should be an annotated tag (thus showing the time of creation!) and should be named submission. Don't forget to push your tags (git push origin --tags)if you created them offline.

Here's a checklist of things not to forget:

• Please add both me and Alex to your Project as Reporters, regardless of who your project supervisor was.
• Inline documentation: If you're a group, every code file should have the name(s) of its author(s) at the very top. Comment your code: At least all the statements (theorem, lemma, ...) should have a comment explaining what they do).
• Documentation: Two PDF-files (theory and formalization) per person in the Docs folder.
• Add all necessary info that we might need to run/evaluate your project to the Readme.

Good luck for the remaining week,

Leon

Dear participants,

Next week, on Thursday, Feb. 5th will be the poster session. It will start at 14:00 (s.t.!) and happen right outside the usual lecture hall HS I. Bring your printed posters and hang them in one of the free spots. Alex and me will walk around and have a quick (5-10min) conversation with each group.

As already explained, the content of the poster should be your project, with a lot of freedom. You may find inspiration in the following questions: What is the theory you are formalizing (mathematically)? Are there applications/reasons why it's important to formalize them? Which concepts in Lean/mathlib are you going to use? Are you planning on specific models for some definitions?

Poster size should be either DIN A2 or A3. Posters can be hand-written/-drawn or printed (or anything else, really, if it supports the presentation). Please have the names of all group members on the poster.

During the session, you are highly encouraged to look at the other posters and discuss amongst each other - that's what the session is intended for.

See you there,

Leon

Dear participants,

I'm happy to inform you that next week's seminar session will feature a guest talk by Rida Hamadani, about their extensive experience in using Lean both in the mathematical community as well as professionally in the industry.

In addition to the talk in the seminar, Rida will give another talk on formalizing specific algebraic topics in Lean, in the Research Seminar of the algebra group, where everybody who is interested is very welcome. This talk will be on Tuesday (27th) at 14.00 (sharp) in HS IV in building E2.4.

Title and abstract of that talk will be published over the next couple days here.

Have a nice weekend,

Leon

 

PS: While I promised to share a link to the university poster latex templates, it seems like these are no longer publicly available. However, a quick websearch is going to provide you with plenty of other examples, and I suppose GenAI is reasonably good at LaTex these days ;)

Dear participants,

There is now a git repository with a project template for your seminar project, to be found here: https://gitlab.cs.uni-saarland.de/pernak/fmil26

For your individual project you should fork the project above. Read the Readme file in the root folder for further instructions on how to structure your files.

Also, once you have created the project add me (@pernak) to the repository as a reporter. If Alex is your project instructor, add him (@alik00001) too.

If Alex is your instructor, you can now also find his E-Mail on the "Team" page in CMS.

Lastly, there is now a Forum on the CMS Page. You can use it to find project partners or share inspirations for projects, and ask questions.

Happy leaning, see you on Thursday.

Leon