Patrick Reany
28 November 2023
I had this conversation with BingChat on 27 November 2023.
Hold on! Update! [20 February 2024] I only just recently learned of the fascinating Microsoft program
called Lean. Lean is perhaps the most excitiing thing to come along in computer-aided
mathematics in a generation!You can read up about it on Wiki and also on the website of mathematician Kevin Buzzard.
https://www.imperial.ac.uk/people/k.buzzard
Copilot gave me the following references for websites specializing in Lean [slightly edited]:
LeanDojo: LeanDojo introduces Lean Copilot, which acts as a copilot for theorem proving within Lean.
It suggests tactics, premises, and even searches for proofs. You can use their pre-trained model or bring
your own models to enhance your Lean experience. LeanDojo also provides a benchmark dataset extracted
from math libraries, enabling fine-grained premise annotations and challenging data splits.https://leandojo.org/
Five free resources to get you started with the Lean Theorem Prover: If you’re just beginning,
this concise list provides free resources to kickstart your journey into programming proofs using Lean.https://medium.com/@andrewlubrino_74588/five-free-resources-to-get-you-started-with-the-lean-theorem-prover-823af16f58d6
Lean Official Website: For comprehensive information, visit the official Lean website. It covers both
the programming language and the theorem prover aspects of Lean.https://lean-lang.org/
Tutorial: Theorem Proving in Lean: Dive deeper into Lean with this tutorial, which focuses on
automated theorem proving and provides practical insights.https://leanprover.github.io/tutorial/
This link takes you to a YouTube video by Computerphile on Lean:https://www.youtube.com/watch?v=prYaTrZUces
Patrick:
What is a proof assistant in computer science and mathematics?
BingChat:
A proof assistant or interactive theorem prover is a software tool that assists with the development
of formal proofs by human-machine collaboration [1]. It is used in computer science and mathematical
logic to verify the correctness of mathematical proofs. A proof assistant provides an interactive proof
editor or other interface, with which a human can guide the search for proofs, the details of which
are stored in, and some steps provided by, a computer [1].
Proof assistants are increasingly used in all areas where mistakes are not an option, such as
in the design of hardware components, software programs, or to produce machine-checked proofs of
deep results in mathematics [2].
Some examples of proof assistants include Coq, Isabelle, and HOL Light [1].
1: Wikipedia 2: International Summer School on Interactive Theorem Proving
Patrick:
A few months ago, I used BingChat to help me prove a result in mathematics. Are you officially
considered as a proof assistant?
BingChat:
I'm glad to hear that you found BingChat helpful in your mathematical proof. However, I am not
officially considered as a proof assistant. I am a conversational AI designed to assist with a
wide range of tasks, including answering questions, providing information, and generating creative
content such as poems, stories, code, essays, songs, celebrity parodies, and more. While I can
help you with your mathematical proofs, I am not a substitute for a formal proof assistant like
Coq, Isabelle, or HOL Light .
If you have any other questions or need help with anything else, feel free to ask!
Patrick:
Okay, then what is the main difference between BingChat as an 'informal proof assitant' and the
formal proof assistants such as Coq, Isabelle, or HOL Light? In other words, what do they
have that you don't?
BingChat:
The main difference between BingChat and formal proof assistants such as Coq, Isabelle, or HOL
Light is that the latter are designed specifically for the purpose of verifying the correctness
of mathematical proofs. They provide a more comprehensive set of tools and features for this task,
including a formal language for expressing mathematical statements and proofs, a library of
mathematical definitions and theorems, and a set of tactics or strategies for guiding the search
for proofs [1].
In contrast, BingChat is a conversational AI designed to assist with a wide range of tasks,
including answering questions, providing information, and generating creative content such as
poems, stories, code, essays, songs, celebrity parodies, and more. While I can help you with
your mathematical proofs, I am not a substitute for a formal proof assistant like Coq, Isabelle,
or HOL Light [2].
That being said, BingChat has some unique advantages over formal proof assistants. For example,
it is more accessible and user-friendly, requiring less technical expertise to use effectively.
It is also more flexible and adaptable, able to handle a wider range of tasks and contexts than
a formal proof assistant [3].
I hope that helps! Let me know if you have any other questions or need help with anything else.
1: Wikipedia 2: Wikipedia 3: Zapier [https://zapier.com/blog/chatgpt-vs-bing-chat/]
Patrick:
In other words, one of the advantages of my using an LLM is that I don't have to learn a
formal syntax to use with one of those formal proof assistants.
BingChat:
Yes, that’s correct. One of the advantages of using a proof assistant like Coq, Isabelle,
or HOL Light is that it provides a formal language for expressing mathematical statements
and proofs. However, this formal language can be quite complex and requires a significant
amount of time and effort to learn.
In contrast, BingChat does not require you to learn a formal syntax to use it effectively. Instead,
you can simply type in your mathematical statements and proofs in natural language, and
BingChat will help you to refine and formalize them as needed. This makes it much more
accessible and user-friendly than a formal proof assistant, especially for those who are new
to the field of mathematical logic [1,2].
That being said, formal proof assistants like Coq, Isabelle, or HOL Light have some unique
advantages over BingChat. They provide a more comprehensive set of tools and features for
verifying the correctness of mathematical proofs, including a library of mathematical definitions
and theorems, a set of tactics or strategies for guiding the search for proofs, and a formal language
for expressing mathematical statements and proofs [1].
I hope that helps! Let me know if you have any other questions or need help with anything else.
1: Wikipedia 2: Zapier
Patrick:
Which companies or universities created each of Coq, Isabelle, and HOL Light?
BingChat:
Coq was created in 1984 by a group of researchers at the French national research institute
INRIA, led by Thierry Coquand [1]. Isabelle was developed in the late 1980s by a team of
researchers at the University of Cambridge and the Technical University of Munich, led by
Lawrence Paulson [2]. HOL Light was created in the early 1990s by John Harrison at the
University of Cambridge [3].
I hope that helps! Let me know if you have any other questions or need help with anything else.
1: Wikipedia 2: Wikipedia 3: Wikipedia
Patrick:
Has any one of those programs been credited with helping to verify any important theorems
in the last 40 years? If so, what references can you provide?
BingChat:
Yes, all three proof assistants, Coq, Isabelle, and HOL Light, have been credited with helping
to verify important theorems in the last 40 years. Here are some examples:
Coq was used to formalize the proof of the four-color theorem in 2005 by Georges Gonthier and
Benjamin Werner [1].
Isabelle was used to formalize the proof of the Kepler conjecture in 2014 by Thomas Hales and
his team [2].
HOL Light was used to formalize the proof of the Feit-Thompson theorem in 2012 by Georges Gonthier
and his team [3].
These are just a few examples of the many important theorems that have been verified using proof
assistants. I hope that helps!
1: Wikipedia 2: Wikipedia 3: Wikipedia
Patrick:
Above, you used Zapier as a reference. Please explain to me what this Zapier is all about.
BingChat:
Certainly! Zapier is an online automation tool that connects your apps and services. It allows
you to automate repetitive tasks without coding or relying on developers to build the integration [1,2].
Zapier works by letting you create Zaps, automated workflows that consist of a trigger and one
or more actions. When you set up and activate a new Zap, it will run its action(s) every time the trigger
event occurs [3].
Zapier has many subscription levels, ranging from free for individual users to plans for teams and
entire organizations [1]. It integrates with over 2000+ destinations other than Twitter, including
Facebook, Pinterest, and many more [3].
Some examples of what you can do with Zapier include automatically sending out a custom tweet right
after you’ve published a post, creating a new Trello card when a new email arrives in your inbox, or
saving new Gmail attachments to Dropbox [3].
I hope that helps! Let me know if you have any other questions or need help with anything else.
1: Business Insider 3: Yoast 2: Zapier
------------------------
Note 1:
The Feit-Thompson theorem, also known as the odd order theorem, is a result in mathematics that states
that every finite group of odd order is solvable [1]. It was proved by Walter Feit and John Griggs
Thompson in 1962 and 1963 [1]. The theorem is an important result in the classification of all finite simple
groups, and it states that every non-Abelian simple group must have even order [1]. According to Feit and
Thompson, every finite simple group (that is not cyclic) has even group order, and the group order of
every finite simple noncommutative group is doubly even, i.e., divisible by 4 [1]. (Provided by BingChat.)
Note 2:
The Kepler conjecture concerns the average density of possible arrangements of spheres in a 3d space.