Η παρούσα διπλωματική εργασία εστιάζει στην ανάπτυξη, υλοποίηση και αξιολόγηση ενός συστήματος αυτόματης απόδειξης μαθηματικών θεωρημάτων στη γλώσσα Lean 4, αξιοποιώντας Μεγάλα Γλωσσικά Μοντέλα (Large Language Models – ...