Lean 4 và bài toán verify toán tài chính bằng proof chính thức

Mình đọc paper này lần đầu và phản ứng đầu tiên là: "Ủa, ai cần verify toán tài chính bằng proof assistant làm gì?" Nhưng ngồi nghĩ lại một lúc, thấy cái này thực ra khá thú vị đặc biệt với anh em đang làm trong mảng fintech hoặc quantitative finance.

Paper có tên "A Formally Verified Library of Mathematical Finance in Lean 4" vừa drop, và về cơ bản đây là một thư viện Lean 4 chứa các định lý toán tài chính đã được formally verified tức là không phải "mình test thấy đúng" hay "paper toán học nói vậy", mà là máy tính đã kiểm tra từng bước logic và xác nhận proof là hợp lệ.

Lean 4 là gì và tại sao dân finance lại cần nó?

Nếu bạn chưa biết, Lean 4 là một proof assistant một ngôn ngữ lập trình kiêm hệ thống logic cho phép bạn viết các mathematical proof và để máy tính verify chúng. Khác với unit test ("tôi chạy thử 1000 trường hợp, không thấy bug"), formal verification nói rằng "tôi chứng minh được về mặt toán học rằng điều này đúng với mọi trường hợp có thể xảy ra".

Thư viện này được build trên hai nền tảng:

• Mathlib thư viện toán học lớn nhất của Lean 4, cover từ algebra đến topology
• Degenne's BrownianMotion một formalization của chuyển động Brown, thứ nằm ở trái tim của hầu hết mọi model định giá option

Combination này cho phép họ formalize các khái niệm như arbitrage-free pricing, martingale theory, và các kết quả liên quan đến stochastic calculus.

Tại sao điều này không chỉ là "toán học cho vui"

Mình biết nhiều anh em đọc đến đây sẽ nghĩ: "Oke hay đấy, nhưng mình đang code microservice, cái này liên quan gì?"

Thực ra liên quan nhiều hơn bạn nghĩ, đặc biệt khi nhìn vào bức tranh lớn hơn:

1. Các lỗi trong financial software cực kỳ tốn kém

Knights Capital Group mất 440 triệu USD trong 45 phút năm 2012 vì một bug trong trading algorithm. Không phải logic sai, không phải business rule sai chỉ là một đoạn code deploy không đúng cách. Nhưng còn những lỗi ở tầng sâu hơn, ở tầng mathematical model? Những thứ đó thậm chí khó detect hơn.

2. Regulatory pressure ngày càng tăng

Các cơ quan như SEC, FCA đang yêu cầu các tổ chức tài chính phải có khả năng explain và justify các model của họ. Formal verification cung cấp một loại "audit trail" ở cấp độ toán học mà không có cách nào khác làm được.

3. Smart contracts và DeFi

Nếu bạn đang làm trong mảng blockchain/DeFi, cái này cực kỳ relevant. Các protocol DeFi như Uniswap, Aave về bản chất là mathematical finance implemented as code. Một bug trong pricing formula của AMM có thể drain toàn bộ liquidity pool. Formal verification chính là hướng đi mà nhiều security researcher đang push.

So sánh các approach verify correctness trong financial software

Nhìn bảng này thì rõ ràng formal verification không phải silver bullet chi phí cao, cần người có background toán học + functional programming. Nhưng với những component critical nhất, nó là thứ duy nhất cho bạn guarantee thực sự.

Cái mình thấy thú vị nhất trong approach này

Theo kinh nghiệm của mình khi làm với các financial system, vấn đề lớn nhất không phải là code sai mà là translation từ mathematical specification sang code. Một quant analyst viết ra một formula trên giấy, một developer implement nó thành code, và trong quá trình đó có vô số chỗ có thể "lost in translation".

Cái hay của Lean 4 là nó bridge hai thế giới này lại. Mathematical proof và executable code không còn là hai thứ riêng biệt nữa. Khi bạn prove một theorem trong Lean, bản thân proof đó là code có thể chạy được (hoặc extract ra code).

Cụ thể với paper này, họ formalize các kết quả như:

• No-arbitrage conditions
• Fundamental theorem of asset pricing
• Các properties của martingale trong continuous time

Những thứ này là foundation của hầu hết mọi pricing model trong finance hiện đại. Khi foundation được verify, bạn có một base vững chắc hơn nhiều để build lên.

Lean 4 ecosystem đang phát triển nhanh hơn bạn nghĩ

Anh em lưu ý Lean 4 không còn là thứ chỉ các giáo sư toán học dùng nữa. Mathlib hiện tại có hàng chục nghìn lemma và theorem đã được verify. Microsoft Research đang đầu tư vào đây. Amazon đang dùng formal methods để verify các property của AWS services.

Và quan trọng hơn, các paper liên quan được Librarian Bot recommend cùng với paper này cho thấy một trend rõ ràng:

• Black-Scholes Implied Volatility explicit solutions
• AMM characterization từ swap axioms đến weighted geometric means
• Bachelier option pricing analytic approximations
• Stochastic Volatility với Jumps PIDE framework

Tất cả đều đang được formalize và verify. Đây không phải coincidence đây là một movement có hệ thống để đặt mathematical finance trên nền tảng vững chắc hơn.

Thực tế thì bạn có cần học Lean 4 không?

Mình sẽ thành thật: không phải ai cũng cần. Lean 4 có learning curve khá dốc, đặc biệt nếu bạn chưa quen với functional programming hay type theory.

Nhưng nếu bạn:

• Đang build pricing engines hoặc risk models
• Làm DeFi protocol development
• Research trong quantitative finance
• Quan tâm đến program verification nói chung

...thì ít nhất nên hiểu what formal verification can and cannot do. Không nhất thiết phải tự viết proof, nhưng biết cách use một verified library là valuable skill.

Về mặt practical, cách tiếp cận hợp lý nhất hiện tại là: dùng các verified libraries như thư viện trong paper này làm reference implementation hoặc specification, sau đó implement bằng ngôn ngữ production của bạn (Python, Rust, C++) và test against the verified spec.

Cái workflow này không yêu cầu bạn viết proof, nhưng vẫn cho bạn hưởng lợi từ formal verification work của người khác.

Lean 4 vs các proof assistant khác

Lean 4 đang win về mặt community momentum và tooling quality. Mathlib là competitive advantage lớn nhất nó có breadth và depth mà các hệ thống khác khó match.

Mình nghĩ hướng đi của paper này rất đúng. Thay vì cố gắng verify toàn bộ một trading system (unrealistic), họ focus vào mathematical core những theorem nền tảng mà mọi thứ khác build lên. Đó là cách tiếp cận pragmatic và có impact thực sự.

Nếu bạn tò mò muốn xem thử Lean 4 trông như thế nào, có thể vào leanprover-community.github.io và chơi với online editor. Không cần install gì cả. Cái syntax ban đầu trông khá lạ nếu bạn quen với imperative languages, nhưng sau vài tiếng thì bắt đầu click.