中國科學院數學機械化重點實驗室

中國科學院數學機械化重點實驗室依託：中國科學院數學與系統科學研究院。

"數學機械化"是我國數學家吳文俊先生在七十年代末開始倡導的一個研究領域，是腦力勞動機械化在數學科學的學術實踐。數學機械化思想繼承了中國古代數學的傳統，它的著眼點在數學，但又具有明顯的交叉性。

所謂機械化是指刻板化與規格化。十七世紀以來，以蒸氣機為代表的工業革命是以機器代替人的體力勞動，數學機械化則是用計算機部分代替人類的腦力勞動。今天電子計算機的飛速發展使得數學的機械化正在逐步成為現實。在數學發展過程中，可以看到演繹傾向與演演算法傾向的此消彼長。兩種傾向總是交替地處於主導地位。值得注意的是，探詢新演演算法可以導致數學的重大發現，如解析幾何與微積分；而且構造性數學往往具有很高的實用價值。數學機械化研究的深入開展，不僅會進一步豐富數學科學的傳統內容，也將進一步豐富其交叉性學科的內容，從而在總體上促進數學科學的發展。

數學機械化不僅是數學研究的實質性進展，也為很多高科技問題的解決提供了有力的工具。我們的方法已在許多高科技領域獲得了一批理論成果，具備了解決尖端技術產業中實際問題的條件。包括曲面造型，機器人位置分析，幾何設計，計算機視覺，智能CAD，信息安全和數字圖象的高速高保真傳輸。通過進一步努力，這些理論研究成果有望能夠實實在在地解決若干項技術問題為促進我國技術產業的發展做出積極的貢獻。

數學機械化研究又有明顯的交叉性。除高科技領域外，數學機械化的方法還被成功地用於解決其他領域的很多問題：理論物理中的楊振寧－Baxter方程求解，天體力學中共心多體問題，化學平衡中的方程求解，小波構造的優化，命題邏輯與一階謂詞邏輯中的定理證明，非線性發展方程的行波解的演演算法等等。

在國際上，計算機與數學的交叉正在成為數學研究新的增長點，出現了計算代數、計算群論、計算幾何、計算數論等新興學科。符號計算是研究在計算機上進行準確的數學演算和與之相關的數學理論的學科，是數學機械化的主要工具。一批專業化的學術機構已在世界各地紛紛成立。符號計算軟體Maple, Mathematica已經在數學與工程領域被廣泛使用。80年代以來，解（微分）代數多項式方程組是國際符號計算界的熱點，其主要方法是Groebner基方法。90年代歐共體跨國研究項目 POSSO(POlynomial System SOlving) 及作為POSSO的延續項目FRISCO關注的問題，與我們開展數學機械化研究課題有許多相同之處。所不同的是，我們所用的是我國數學家自己發展起來的一套方法和理論。

自動推理是與數學機械化密切相關的學科。自動推理源於人工智慧，主要研究推理的自動化與機械化。國外主要以邏輯為基礎開展自動推理研究，而吳方法的基礎是代數幾何。國際上自動推理界在注意發展新方法的同時，積極開展應用研究，如程序正確性驗證，自動程序生成等。

1990年，中國科學院在批准成立數學機械化中心。數學機械化中心建立以來，取得了一系列高水平的科研成果，並獲得了十項國內重要獎勵與兩項國際獎勵。特別值得指出的兩項獎勵是（1）吳文俊先生獲1997年自動推理最高獎"Herbrand自動推理傑出成就獎"。這一榮譽進一步表明吳方法已經被國際學術界認為是自動推理領域最基本與經典性工作。（2）由於在數學機械化與拓撲學方面的傑出貢獻，吳文俊先生於2000年獲得首屆"國家最高科學技術獎"。

數學機械化研究得到國家領導部門的充分肯定和大力支持。國家科技部在"21世紀科學發展趨勢"的報告中將數學機械化列為重大科學問題，國家自然科學基金委員會和中國科學院在"九五"規劃中，都將數學機械化列為優先發展的研究領域。數學機械化中心作為主要承擔單位，主持了八五國家攀登計劃項目"機器證明及其應用"，九五攀登項目"數學機械化及其應用"與"973"項目"數學機械化與自動推理平台"，並以這些項目為依託積極組織國內外數學機械化合作研究與學術交流。經過十多年的努力, 數學機械化中心已經成為國際數學機械化研究、學術交流與人才培養的中心。 2003年, 數學機械化中心與信息安全中心聯合成立了數學機械化重點實驗室。當前信息技術正在給社會生產力帶來一場革命，但由於大量敏感信息通過網際網路進行交換，信息的不安全性帶來嚴重的社會問題。信息安全理論是研究信息在傳輸或存儲過程中保證信息的"可靠性"、"完整性"、"秘密性"、"真實性"等要求的一門科學，它以數學和計算機科學等學科為基礎，現代密碼學和糾錯編碼理論等都是信息安全理論的基礎。密碼學自1976年Differ和Hellman提出公鑰密碼體制以來得到了迅猛發展。1985年Koblitz和Miller提出將橢圓曲線用於公鑰密碼體制，他們第一次用橢圓曲線成功地實現了已有的一些公鑰密碼演演算法包括Differ-Hellman演演算法。橢圓曲線密碼體制不僅是一個重要的理論研究領域，而且已經作為民用信息安全技術走向產業化。

近二十年來，數學和計算機科學中的一些強有力工具和最新研究成果被用到編碼理論和密碼學中，不僅促進了編碼理論和現代密碼學的飛速發展，也刺激了數學和計算機科學中的一些分支的發展。 (1)利用代數組合、代數數論、計算代數和有限幾何的經典工具和最新成果來研究信息科學，特別是編碼理論，在當前是數學家和通信技術專家的公同的領域，也是信息科學中的一個熱門的研究方向。 (2) 代數幾何碼是上世紀八十年代由蘇聯數學家發現的，這一發現使數學中最抽象的分支之一――代數幾何，通過編碼理論被天才地用到通信工程中去。由於代數幾何碼的卓越的糾錯和檢錯性能，持續二十多年，代數幾何碼的研究仍然是資訊理論中的一個熱點。 (3)Turbo碼是法國學者1993年發現的一種新的差錯控制碼，這種碼的糾錯性能幾乎接近Shannon限，在諸如遠程數據通信、數據的磁記錄等廣泛的應用領域是性能最好的碼。 (4) 時空碼（即Space-Time碼）是美國學者Tarokh 和 Calderbank 等人幾年前發現的一種碼，它用在多通道、多天線、無線通信通道--例如手機通信中，可以極大地改進這些通道的性能。 (5) 計算的複雜性理論和Shannon的資訊理論是現代密碼學的兩大理論支柱。複雜性理論作為數學和信息科學共同的領域，將受到更加廣泛的關注。 (6) 量子糾錯碼和量子密碼是量子資訊理論的兩個基本方面，它們都基於量子計算和量子演演算法。研究量子計算和量子演演算法是當今信息科學中的最前沿方向之一。

本實驗室以基礎研究為主，同時兼顧應用研究，採取基礎研究帶動應用研究的思路。研究方向可以分為：理論與方法研究，應用研究與智能軟體開發。

具體講

（1）理論與方法研究：構造性代數幾何，構造性微分代數幾何，構造性實代數幾何，計算機代數，編碼密碼理論，離散幾何，量子計算與方法，代數方程求解的混合演演算法，自動推理；

（2）應用基礎研究：信息安全，在理論物理、力學中的應用，在機器人中的應用，幾何自動作圖與智能CAD，計算機視覺中的應用，信息安全與密碼中的應用；

（3）基於吳方法的智能軟體平台的開發。