Mathematical Structures and Formalization(MAT440)
| Course Code | Course Name | Semester | Theory | Practice | Lab | Credit | ECTS |
|---|---|---|---|---|---|---|---|
| MAT440 | Mathematical Structures and Formalization | 7 | 3 | 0 | 0 | 3 | 5 |
| Prerequisites | |
| Admission Requirements |
| Language of Instruction | |
| Course Type | Elective |
| Course Level | Bachelor Degree |
| Course Instructor(s) | Ayberk ZEYTİN azeytin@gsu.edu.tr (Email) |
| Assistant | |
| Objective | - |
| Content |
Overview of functional programming, Types, Terms, Equality, di?erent kinds of types, structures, classes Setting up well-known mathematical structures in Lean, proving well-known theorems via Lean |
| Course Learning Outcomes |
1. Understand the need for a formalism in mathematics. 2. To learn functional programming basics 3. To be able to use proof assistants |
| Teaching and Learning Methods | Face to face or online |
| References |
How To Prove It (with Lean), Daniel J. Velleman Theorem Proving in Lean 4, Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich, |
Theory Topics
| Week | Weekly Contents |
|---|---|
| 1 | Overview and Installation |
| 2 | Lean Syntax and Proof Interface |
| 3 | Logic Review in Lean |
| 4 | Proof Tactics and Style |
| 5 | Structures and Type Classes |
| 6 | Inductive Types and Recursion |
| 7 | Proofs by Induction |
| 8 | Sets and Relations |
| 9 | Algebraic Hierarchy |
| 10 | Number Theory in Lean I |
| 11 | Number Theory in Lean II |
| 12 | Finite Structures and Combinatorics I |
| 13 | Finite Structures and Combinatorics II |
| 14 | Analysis in R |
Practice Topics
| Week | Weekly Contents |
|---|---|
| 1 | --- |
| 2 | --- |
| 3 | --- |
| 4 | --- |
| 5 | --- |
| 6 | --- |
| 7 | --- |
| 8 | --- |
| 9 | --- |
| 10 | --- |
| 11 | --- |
| 12 | --- |
| 13 | --- |
| 14 | --- |
Contribution to Overall Grade
| Number | Contribution | |
|---|---|---|
| Contribution of in-term studies to overall grade | 6 | 60 |
| Contribution of final exam to overall grade | 1 | 40 |
| Toplam | 7 | 100 |
In-Term Studies
| Number | Contribution | |
|---|---|---|
| Assignments | 0 | 0 |
| Presentation | 6 | 60 |
| Midterm Examinations (including preparation) | 0 | 0 |
| Project | 0 | 0 |
| Laboratory | 0 | 0 |
| Other Applications | 0 | 0 |
| Quiz | 0 | 0 |
| Term Paper/ Project | 0 | 0 |
| Portfolio Study | 0 | 0 |
| Reports | 0 | 0 |
| Learning Diary | 0 | 0 |
| Thesis/ Project | 0 | 0 |
| Seminar | 0 | 0 |
| Other | 0 | 0 |
| Make-up | 0 | 0 |
| Toplam | 6 | 60 |
| No | Program Learning Outcomes | Contribution | ||||
|---|---|---|---|---|---|---|
| 1 | 2 | 3 | 4 | 5 | ||
| Activities | Number | Period | Total Workload |
|---|---|---|---|
| Class Hours | 14 | 3 | 42 |
| Working Hours out of Class | 14 | 3 | 42 |
| Assignments | 0 | 0 | 0 |
| Presentation | 3 | 5 | 15 |
| Midterm Examinations (including preparation) | 0 | 0 | 0 |
| Project | 0 | 0 | 0 |
| Laboratory | 0 | 0 | 0 |
| Other Applications | 0 | 0 | 0 |
| Final Examinations (including preparation) | 1 | 36 | 36 |
| Quiz | 0 | 0 | 0 |
| Term Paper/ Project | 0 | 0 | 0 |
| Portfolio Study | 0 | 0 | 0 |
| Reports | 0 | 0 | 0 |
| Learning Diary | 0 | 0 | 0 |
| Thesis/ Project | 0 | 0 | 0 |
| Seminar | 0 | 0 | 0 |
| Other | 0 | 0 | 0 |
| Make-up | 0 | 0 | 0 |
| Yıl Sonu | 0 | 0 | 0 |
| Hazırlık Yıl Sonu | 0 | 0 | 0 |
| Hazırlık Bütünleme | 0 | 0 | 0 |
| Total Workload | 135 | ||
| Total Workload / 25 | 5.40 | ||
| Credits ECTS | 5 | ||