形式證明是一種推理方法，它通常涉及使用形式化語言或符號邏輯來構建和展示一個命題從公理系統中的已知定義及其他定理推導出來的過程。以下是關於形式證明的幾個關鍵點：
邏輯系統內的證明：在邏輯系統τ內，如果有一合式公式的有窮序列A1,A2……An-1,An，其中每一項或是系統內的公理，或是由序列中的先前公式根據系統的變形規則而得到的，那麼這個合式公式的有分序列就是τ系統內的一個形式論證。
形式化語言的使用：形式證明著重於使用形式化語言來構建完整的證明過程，從而保證其正確性。這種語言的使用可以消除人為判斷、主觀意見等因素的干擾，並嚴格地驗證每一步推理。
與嚴格證明的關係：形式證明通常被視為一種特殊的嚴格證明。嚴格證明是一種更廣義的概念，它可以包括形式證明在內，也可以指其他類型的證明。
計算機科學中的套用：在計算機科學中，形式證明通常指的是使用互動式定理證明器等工具，通過機器驗證推理過程來證明一個命題的真實性。這種證明方式可以提高證明的可靠性和可重複性。
形式與實質性的區別：形式證明關注的是數學表達式的表面形式，而不去注意裡面的符號究竟都代表什麼，或者不去檢查其適用範圍。這與實質性的推理方法不同，後者更注重推理的實質內容。
以上是對形式證明的概述，希望對你有所幫助。