Math AI Lab University of Washington A guide to Math AI background material, UW courses, and related seminar series.
theorem Matrix.luFactorization_reconstruct
(M : Matrix (Fin a) (Fin b) R) :
let lu := Matrix.luFactorization M
lu.P * lu.L * lu.U = M := by
simpa [Matrix.luFactorization] using
LUFactorizationInternal.rawFactorization_reconstruct (R := R) (M := M)
theorem Matrix.luFactorization_upper_isEchelonForm
(M : Matrix (Fin a) (Fin b) R) :
IsEchelonForm (M := (Matrix.luFactorization M).U) := byMath AI-related colloquia and seminars at the University of Washington.
We often hear that mathematics consists mainly of proving theorems. Is a writer's job mainly that of writing sentences?
-- Gian-Carlo Rota (1980)
Math AI-related colloquia and seminars at University of Washington
Formal methods, AI and machine learning, NLP, optimization, data science, and ethics courses.
Rigor has ceased to be thought of as a cumbersome style of formal dress that one has to wear on state occasions and discards with a sigh of relief as soon as one comes home. We do not ask any more whether a theorem has been rigorously proved but whether it has been proved.
-- André Weil (1956)
Background material, Math AI reading, and Lean resources for getting started and getting serious.
"Investing in applied machine learning without understanding the mathematical foundations is like investing in health care without understanding biology".
-- Rebecca Willett (2023)
What is Math AI? At the intersection of mathematics and AI is a broad, rapidly-developing subject. It is truly interdisciplinary subject connected to mathematics, applied mathematics, statistics, computer science, philosophy, and engineering. It can be roughly categorized into five interrelated areas: