要使計算機能夠處理和解決數學問題，需要有指導計算機硬件設備執(zhí)行運算的特殊數據和指令。這樣的數據和指令集就是數學軟件，也就是處理數學對象（包括數學計算、推理、繪圖、文本制作等）的計算機程序。這里數學對象有數值、符號、圖形等多種類型。由于數學任務種類繁多，數學軟件也形式各異。

數學對象的表示

為了簡明地表示數學概念及其邏輯結構，數學家引進了很多特殊的數學符號，如積分號、求和號、根號，并約定了相應的表達方式和結構，如上下標、分式等。這些符號和表達結構使數學表達式具有不同于普通文字線性排列的二維結構。數學內容要在計算機上存儲和呈現，就必須按照特定格式或語言對其進行編碼。最廣泛使用的編碼格式當屬著名計算機科學家Donald E. Knuth發(fā)明的。

通過一系列基本的文本命令將復雜的數學公式線性化，并允許利用這些命令定義更復雜的高級命令，從而得到更易于用戶使用的編碼格式。美國計算機科學家Leslie Lamport在20世紀80年代初設計開發(fā)了后來廣泛使用的及其優(yōu)化版本。利用及改進的排版系統(tǒng)可以對和命令進行編譯并生成高質量的dvi、pdf、ps等格式的可顯示文件，打印輸出。

為了使數學表達式能通過互聯(lián)網傳播和處理，萬維網聯(lián)盟W3C的數學工作組于1998年制定并發(fā)布了MathML標記語言，作為通過互聯(lián)網交流數學符號和公式的標準規(guī)范。目前MathML已發(fā)展到第三代，與前二代相比，其表達能力更強、范圍更廣，并得到了Mozilla Firefox、Camino等瀏覽器的支持。以MathML編碼的數學公式能夠在網頁中以可讀的形式呈現，而Safari、Chrome、Opera、InternetExplorer等瀏覽器都曾經支持過MathML編碼的網頁，但出于安全和穩(wěn)定性的考慮，目前已不再支持。又為了使數學內容與所有瀏覽器都兼容，MathJax聯(lián)盟開發(fā)了一款JavaScript程序，可以將MathML和編碼的數學表達式動態(tài)地轉化為HTML或者SVG格式，再通過CSS樣式表呈現出來。除了以上側重于數學表達式呈現結構的編碼格式之外，還有一類針對數學表達式語義的編碼語言，如OpenMath標記語言，它通過Content Dictionaries（CD）指明數學符號的語義，從而使數學表達式可以在不同數學軟件系統(tǒng)之間交互、共享和使用。例如，定積分表達式用編碼為＄\int_0^1 e^x dx＄，而使用MathML和OpenMath編碼則是一連串的一元（相當于“如果就”,以滿足硬件的“一元二碼”，它是物理學研究的本質問題）線性邏輯程序。

另一方面，要利用計算機程序對數學對象進行計算和推理，還需要針對其特征設計合適的數據結構。例如，32位計算機能夠處理的最大整數（無符號）是2³²-1，更大的整數如何在計算機上表示是開發(fā)數學計算軟件所要解決的基本問題。事實上，假設B是一個大于1的整數，那么任何一個正整數a在B進制下都可以唯一地表示為

式中表示a在B進制下的每一位。為了表示大整數，首先可以將B取得很大，比如可以令B-1為計算機所能表示的最大整數，然后用一個序列（如數組）來存儲（n+1個整數）。由于這個序列的長度可以很大，如果令n+1為計算機所能表示的最大整數，那么這種方式表示的正整數a就可以任意大。

在現有的計算機代數系統(tǒng)中，考慮到效率和實用性，B通常并不需要設得很大就能夠滿足應用需求。同時，這種數據結構還可以在計算機上表示諸具有級數特征的代數對象，通過設計相應的算法便能實現代數運算。

數學計算與推理

計算機中的數學計算分為兩種：數值計算和符號計算。

前者是指帶有（截斷）誤差的浮點數之間的運算，如果運算步驟很多就會造成累計誤差很大，因此數值計算的算法通常需要考慮穩(wěn)定性，即輸入數據的微小擾動是否會引起輸出的大幅波動，還需要考慮算法是否收斂以及收斂的速度如何等問題。

后者是指具有數學含義的抽象符號之間的精確運算，例如分式化簡，函數的級數展開、求導、求積，符號方程求解，曲線曲面求交等，這些符號除了包括整數、數學常數、多項式等代數對象以外，還包括幾何對象、圖形、文本等。由于符號之間的邏輯關系可以很復雜，因此符號計算的算法通常需要考慮如何設計優(yōu)化的數據結構和模型來降低運算的空間與時間復雜度。

數學計算軟件通常由用于解決問題的程序庫和功能模塊組成，種類繁多，各有側重。例如，側重數值計算、分析和建模的Matlab（商業(yè)軟件）、Scilab（開源自由軟件）；側重符號計算、推導和化簡的Maple（商業(yè)軟件）、Mathematica（商業(yè)軟件）。另外還有側重于專門領域的軟件，如SAS（商業(yè)軟件）、R（開源自由軟件）等統(tǒng)計分析軟件；Gams（商業(yè)軟件）、Lingo（商業(yè)軟件）等運籌優(yōu)化軟件；CGAL（開源自由軟件）等離散幾何計算軟件。

數學推理是指從給定的一組被賦予數學含義的抽象符號關系式（即前提）出發(fā)，依據邏輯推理規(guī)則（如三段論）對這些符號關系式進行一系列替換和重排，得到另外一組具有數學含義的抽象符號關系式（即結論）的過程。由于整個過程只是對某些抽象符號進行形式上的操作和處理，因此數學推理在某種意義上也可以看作是一種特殊的符號計算。

數學推理的算法主要考慮如何設計具有嚴格語法規(guī)則的符號系統(tǒng)（即形式化語言，如一階謂詞邏輯語言）來承載數學語義，以及在此基礎上通過怎樣的推理規(guī)則和搜索策略實現從前提到結論的符號演變（這個演變過程即為證明，被證明過的結論即為定理）。數學推理軟件主要分為兩類：自動推理軟件和交互式證明助手。

1）.自動推理軟件是指推理過程能夠自動完成的軟件，有時也稱作自動定理證明器。這類軟件主要包括E、Otter、Vampire、SPASS等支持一階謂詞邏輯語言的通用證明器和適用于具體領域的專用證明器。在使用通用自動定理證明器進行數學推理時，需要將所涉及的全部數學公理（即不證自明的命題）都形式地表示成邏輯公式作為前提，才有可能保證自動推理的順利進行。

然而，實際上這并不容易實現，因為人們在進行數學推理時會默認地應用一些常識性結論，而這些結論對證明至關重要。例如，Euclid《幾何原本》所列出的五條公設和五條公理其實并不完整，必須利用圖形的直觀作為推理的額外依據才能夠得到書中的某些結論。為了填補這個缺陷，David Hilbert在《幾何基礎》一書中提出了一個更加嚴密而完整的平面幾何公理系統(tǒng)。又為了彌補通用自動定理證明器在數學推理上的不足，Theorema系統(tǒng)將數學知識庫與自動定理證明器結合起來，使之不僅擁有一個通用的高階謂詞邏輯證明器，還有一系列領域相關的專用證明器，讓數學推理變得更加友好、高效。除此之外，Mizar系統(tǒng)能夠自動驗證以Mizar語言編寫的數學文檔的邏輯推理正確性，并由此構建了一個包含千余篇形式化文檔的數學知識庫。

在數學的眾多分支中，幾何學是自動推理發(fā)展最為成功的領域之一，這主要歸功于以吳文俊先生為代表的一批中國學者的開創(chuàng)性工作。幾何定理自動證明器數量眾多，并以不同的方法實現了幾何學自動推理。例如，JGEX和超級畫板實現了面積法（將一組與面積大小有關的恒等式作為公理）、全角法（將一組與角度大小有關的恒等式作為公理）、數據庫演繹法（通過雙向推理自動獲得給定圖形所蘊含的所有定理）等幾何不變量方法，能夠自動生成簡潔漂亮的可讀證明；GEOTHER實現了吳方法（將幾何定理證明問題轉化為關于坐標變元的多項式方程組零點包含關系的判定問題）、Gr?bner基方法（將幾何定理證明問題轉化為關于坐標變元的多項式理想和根理想的成員判定問題）等代數方法；Cinderella實現了括號代數法；GeoGebra實現了實例檢測法。

2）.交互式證明助手是指推理過程需要人機交互協(xié)作完成的軟件。這類軟件主要有Coq和Isabelle/HOL等，能夠在保證推理正確的前提下，幫助用戶構造形式化的證明，并可以從構造過程中自動生成可信的計算程序。正是由于所構造的證明具有高可信度，證明助手已被廣泛應用于航空航天、武器裝備、醫(yī)療設備、交通、核能、金融等安全攸關軟件系統(tǒng)的可靠性驗證。

盡管人們利用證明助手構建了一些初等數學理論的形式化知識庫（包含公理、定義、定理、證明等），也構造出如四色定理等數學難題的形式化證明，然而在實際應用中，證明助手還沒有被數學家廣泛使用。其原因主要有兩方面：一是構造形式化證明的成本太高，除了要學習具有精確語法的形式化語言來編碼數學知識，還要保證每步推理都必須嚴格有據，這就使得證明必須從相關的所有原始公理（或被證明過的定理）出發(fā)一步一步地有序進行，不然不恰當的策略會導致證明無路可走，甚至會出現循環(huán)證明的情況；另一方面是推理工具的自動化程度不高，形式化的證明與程序代碼沒有本質區(qū)別，晦澀而繁雜，在構造證明的過程中會頻繁使用已經證明過的定理，目前并沒有高效的定理搜索和策略推薦等自動化工具來輔助指導證明的構造。

因此，交互式證明助手目前在數學上的應用還處于初級階段。隨著形式化數學知識的不斷累積，以及能夠有效管理知識的自動化工具的出現，交互式證明助手終將成為數學家的好幫手。

人機交互界面

數學軟件一般都提供可通過鼠標、鍵盤或觸控等方式進行操作的人機交互界面，這種人機交互主要包括以下三類。

1）.文本編輯：通過鍵盤輸入數學符號、圖形、圖表等編碼后的文本，經過編譯和運行后得到的結果直接返回到當前界面中。如WinEdt GUI、Maple Worksheet、Mathematica Notebook。

2）.按鈕點擊：通過鼠標點擊按鈕得到相應數學符號的編碼文本（如、MathML），一般還會以所見即所得（WYSIWYG）的方式將數學符號呈現出來。如MathType、iMathEQ、MathMagic等數學公式編輯器以及LyX、Mathcha等數學文檔編輯器。

3）.手寫識別：通過鼠標、觸控筆或手指在軟件界面上書寫數學表達式，經過專門的程序識別得到相應的數學編碼。如MathBrush、E-chalk、MathPad。

大部分數學計算軟件都具有圖形圖像繪制、函數動態(tài)模擬等可視化功能，并可以進行交互處理，使抽象的數學內容以直觀生動的方式呈現出來。還有一類如GeoGebra、Cinderella、JGEX、超級畫板等與幾何作圖有關的軟件，稱為動態(tài)幾何軟件。利用這些軟件所提供的作圖指令，用戶可以使用鼠標或者觸控筆在軟件界面上精確地繪制出滿足給定約束關系（如平行、垂直）的幾何圖形，當拖動圖形中的某些對象時，整個圖形將被實時地重新繪制并依然保持給定的約束關系。動態(tài)幾何軟件的動態(tài)化和精確性能夠直觀地展示圖形所蘊含的幾何關系特征，并且一般還具有函數、幾何、代數、微積分等計算功能，因此被廣泛應用于教育教學與科學研究。另外還有一類由算法函數庫構成的工具包（如LIBM、PETSc/TAO），它們沒有人機交互界面，需要通過其提供的應用程序接口（API）供其他程序或軟件調用。

數學軟件遠不只本文所列出的這一小部分。隨著移動互聯(lián)和云計算時代的到來，數學軟件正朝著模塊化、并行化和群智化的趨勢發(fā)展，并且互操作的需求正在顯現。在不久的將來，數學軟件會更加深刻地影響和改變科學研究的方式和工程應用的效率。