Mathematics

==== Computing ====
{{Further|Theoretical computer science|Computational mathematics}}
The rise of technology in the 20th century opened the way to a new science: [[computing]].{{Efn|[[Ada Lovelace]], in the 1840s, is known for having written the first computer program ever in collaboration with [[Charles Babbage]]}} This field is closely related to mathematics in several ways. [[Theoretical computer science]] is essentially mathematical in nature. Communication technologies apply branches of mathematics that may be very old (e.g., arithmetic), especially with respect to transmission security, in [[cryptography]] and [[coding theory]]. [[Discrete mathematics]] is useful in many areas of computer science, such as [[Computational complexity theory|complexity theory]], [[information theory]], [[graph theory]], and so on.{{Citation needed|date=December 2022}}

In return, computing has also become essential for obtaining new results. This is a group of techniques known as [[experimental mathematics]], which is the use of ''experimentation'' to discover mathematical insights.<ref>{{Cite web |last1=Borwein |first1=J. |last2=Borwein |first2=P. |last3=Girgensohn |first3=R. |last4=Parnes |first4=S. |date=1996 |title=Conclusion |url=http://oldweb.cecm.sfu.ca/organics/vault/expmath/expmath/html/node16.html |url-status=dead |archive-url=https://web.archive.org/web/20080121081424/http://oldweb.cecm.sfu.ca/organics/vault/expmath/expmath/html/node16.html |archive-date=January 21, 2008 |website=oldweb.cecm.sfu.ca}}</ref> The most well-known example is the [[Four color theorem|four-color theorem]], which was proven in 1976 with the help of a computer. This revolutionized traditional mathematics, where the rule was that the mathematician should verify each part of the proof. In 1998, the [[Kepler conjecture]] on [[sphere packing]] seemed to also be partially proven by computer. An international team had since worked on writing a formal proof; it was finished (and verified) in 2015.<ref>{{cite journal |last1=Hales |first1=Thomas |last2=Adams |first2=Mark |last3=Bauer |first3=Gertrud |last4=Dang |first4=Tat Dat |last5=Harrison |first5=John |last6=Hoang |first6=Le Truong |last7=Kaliszyk |first7=Cezary |last8=Magron |first8=Victor |last9=Mclaughlin |first9=Sean |last10=Nguyen |first10=Tat Thang |last11=Nguyen |first11=Quang Truong |last12=Nipkow |first12=Tobias |last13=Obua |first13=Steven |last14=Pleso |first14=Joseph |last15=Rute |first15=Jason |last16=Solovyev |first16=Alexey |last17=Ta |first17=Thi Hoai An |last18=Tran |first18=Nam Trung |last19=Trieu |first19=Thi Diep |last20=Urban |first20=Josef |last21=Vu |first21=Ky |last22=Zumkeller |first22=Roland |title=A Formal Proof of the Kepler Conjecture |journal=Forum of Mathematics, Pi |date=2017 |volume=5 |page=e2 |doi=10.1017/fmp.2017.1 |s2cid=216912822 |url=https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC |language=en |issn=2050-5086 |access-date=February 25, 2023 |archive-date=December 4, 2020 |archive-url=https://web.archive.org/web/20201204053232/https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC |url-status=live |hdl=2066/176365 |hdl-access=free }}</ref>

Once written formally, a proof can be verified using a program called a [[proof assistant]].<ref name=":1">{{Cite journal |last=Geuvers |first=H. |date=February 2009 |title=Proof assistants: History, ideas and future |url=https://www.ias.ac.in/article/fulltext/sadh/034/01/0003-0025 |journal=Sādhanā |volume=34 |pages=3–4 |doi=10.1007/s12046-009-0001-5 |s2cid=14827467 |doi-access=free |access-date=December 29, 2022 |archive-date=December 29, 2022 |archive-url=https://web.archive.org/web/20221229204107/https://www.ias.ac.in/article/fulltext/sadh/034/01/0003-0025 |url-status=live |hdl=2066/75958 |hdl-access=free }}</ref> These programs are useful in situations where one is uncertain about a proof's correctness.<ref name=":1" />

A major open problem in theoretical computer science is [[P versus NP problem|P versus NP]]. It is one of the seven [[Millennium Prize Problems]].<ref>{{Cite web |title=P versus NP problem {{!}} mathematics |url=https://www.britannica.com/science/P-versus-NP-problem |access-date=December 29, 2022 |website=Britannica |language=en |archive-date=December 6, 2022 |archive-url=https://web.archive.org/web/20221206044556/https://www.britannica.com/science/P-versus-NP-problem |url-status=live }}</ref>