Mittwoch, 30. Dezember 2020
Lean
diegolego, 07:26h
Das erste Programm, das ich schrieb, als ich einen Delphi-Kurs besuchte, war eines, das sich selbst öffnete, wenn man es schloß. Dann dachte ich mir, das wäre doch mal eine Aufgabe für eine KI, ein Programm, das Programme schreibt.
Es hat nicht viel damit zu tun, aber gestern bin ich auf Lean gestoßen. Es handelt sich um einen "proof assistant". In Mathe war ich immer schlecht, aber ich vermute, es soll bei mathematischen Beweisen assistieren.
Jemand hat sich das mal genauer angesehen: A Review of the Lean Theorem Prover. Interessant ist vielleicht noch, daß es von Microsoft entwickelt wird.
Es hat nicht viel damit zu tun, aber gestern bin ich auf Lean gestoßen. Es handelt sich um einen "proof assistant". In Mathe war ich immer schlecht, aber ich vermute, es soll bei mathematischen Beweisen assistieren.
Jemand hat sich das mal genauer angesehen: A Review of the Lean Theorem Prover. Interessant ist vielleicht noch, daß es von Microsoft entwickelt wird.
