Formalni dokaz je zaporedje trditev, besednih ali matematičnih, ki se uporablja za prikaz logične nujnosti določenega zaključka. Takšni dokazi zahtevajo strogo in natančno uporabo jezika, saj lahko jezikovna dvoumnost zlahka naredi dokaz brez pomena. V mnogih primerih, da bi se izognili tej težavi, lahko formalni dokaz predstavimo simbolično ali matematično, da se čim bolj izognemo zmedi, ki jo vnese jezik. Takšni strogo formalni dokazi se običajno začnejo z eno ali več dobro uveljavljenimi ali teoretičnimi predpostavkami. Tem premisam sledijo aksiomi ali trditve, ki logično sledijo prejšnjim trditev in se končajo s končnim zaključkom ali dokazanim izrekom, ki je, tako kot prejšnje trditve, logično nujen rezultat začetnih premis in aksiomov.
V nasprotju s formalnim dokazom se večina argumentov v vsakdanjem življenju opira na skupni jezik in na splošno niso logično strogi. Morda na primer ne izvirajo iz dobro zgrajenega sklopa premis ali pa se lahko zanašajo na retorične pozive – glede čustev ali avtoritete – ki nimajo mesta v formalnem dokazu. Čeprav je formalni dokaz dragocen zaradi svoje sposobnosti, da dokaže pravilnost izjave, ki temelji na nizu premis, je pomembno zapomniti, da imajo formalni dokazi malo ali nič uporabne, ko razpravljamo o nečem, česar ni mogoče dokončno dokazati na področju logike. . Prav tako se uporabljajo samo v kontekstu prvotnih premis in zato ne dokazujejo univerzalnih resnic.
Večina formalnih dokazov temelji na “formalnem jeziku”, sestavljenem bodisi iz podmnožice običajnega jezika bodisi iz simbolov. Matematični formalni dokaz je na primer izražen s simboli, ki se uporabljajo v matematiki, in se sploh ne zanašajo na besedni jezik. V mnogih primerih so besede nadomeščene s simboli, tako da je celo nematematični formalni dokaz mogoče razumeti v obliki preproste simbolne logike brez uporabe potencialno dvoumnih besed.
Veliko različnih področij, običajno v akademskih krogih, uporablja formalne dokaze. Najbolj očiten primer je matematika, področje, ki v veliki meri temelji na uporabi dokazov. Podobno se računalništvo zanaša na uporabo strogih, formalnih logičnih napredkov, da bi zagotovili absolutno natančna navodila za računalnike. Filozofija, zlasti analitična filozofija, se prav tako opira na uporabo formalnih dokazov za dokazovanje pravilnosti različnih filozofskih trditev v kontekstu različnih predhodno uveljavljenih ali teoretičnih premis.