Mathematician – Formal Systems & AI Foundations (Remote Contract)

Über die Rolle

Was wäre, wenn Ihr tiefes Wissen über formale Mathematik direkt beeinflussen könnte, wie die fortschrittlichsten KI-Systeme der Welt schlussfolgern, beweisen und denken? Wir suchen Mathematiker mit einer Leidenschaft für rigorose Beweise und formale Systeme, um die mathematischen Grundlagen zu schaffen, von denen moderne KI abhängt.

Dies ist eine vollständig remote arbeitende, flexible Vertragsrolle an der Schnittstelle von reiner Mathematik, Logik und modernster KI-Forschung. Wenn Sie formale Beweise lieben – und insbesondere wenn Sie sich mit Lean 4 auskennen – ist dies eine seltene Gelegenheit, zur Entwicklung von KI-Frontiers beizutragen, und zwar nach Ihrem eigenen Zeitplan, von überall in Deutschland aus.

• Organisation: Alignerr
• Typ: Stundenbasierter Vertrag
• Standort: Remote
• Engagement: 10–40 Stunden/Woche

Ihre Aufgaben

• Formalisierung fortgeschrittener mathematischer Argumente und Theoreme in Lean 4 über ein breites Spektrum mathematischer Disziplinen hinweg.
• Beitrag zum Wachstum und zur Qualität großer formaler mathematischer Bibliotheken, einschließlich mathlib.
• Erstellung sauberer, lesbarer und gut strukturierter formaler Beweise, die informelles mathematisches Denken in eine rigorose, maschinenprüfbare Form übersetzen.
• Prüfung und Verifizierung bestehender formaler Beweise auf Korrektheit, Vollständigkeit und logische Integrität.
• Arbeit an der Spitze der KI-Forschung, um die nächste Generation mathematisch fähiger Sprachmodelle zu trainieren.

Ihr Profil

• Master-Abschluss oder Promotion in Mathematik oder einem verwandten Fachbereich.
• Starker Hintergrund im Schreiben rigoroser mathematischer Beweise und logischem Denken.
• Praktische Erfahrung mit formalen Beweisassistenten – Lean 4 wird stark bevorzugt.
• Fähigkeit, informelle mathematische Ideen fließend in strukturierte, maschinenverifizierbare formale Beweise zu übersetzen.
• Selbstmotiviert und fähig, unabhängig in einer remote, asynchronen Umgebung zu arbeiten.

Wünschenswert

• Vorerfahrung mit Beweisverifizierung, Theorembeweisen oder Projekten zur mathematischen Formalisierung.
• Vertrautheit mit mathlib oder anderen großen formalen mathematischen Bibliotheken.
• Hintergrund in Datenannotation, Datenqualitätsbewertung oder KI-Trainings-Workflows.
• Erfahrung in verschiedenen mathematischen Bereichen – Topologie, Algebra, Analysis, Logik und mehr.

Warum Sie bei uns einsteigen sollten

• Arbeit an KI-Forschung an der Seite weltweit führender KI-Labore und Forschungsteams.
• Vollständig remote und flexibel – gestalten Sie Ihre Arbeit um Ihr Leben herum.
• Freiberufliche Autonomie mit der intellektuellen Tiefe bedeutungsvoller, anspruchsvoller technischer Arbeit.
• Direkter Beitrag zu formalen mathematischen Bibliotheken, die über einzelne Projekte hinaus Bestand haben.
• Seltene Einblicke in die Entwicklung und das Training modernster großer Sprachmodelle.
• Potenzial für fortlaufende Arbeit und Vertragsverlängerungen bei neuen Projekten.