Questions tagged [mathematics]

Use this tag for questions a mathematician would feel at home answering and can be traced back to an area of mathematics.

Filter by
Sorted by
Tagged with
0 votes
0 answers
50 views

Correcting formally verified results

John Harrison spoke once about checking the results of some peer reviewed mathematical research: he has found bugs in the proofs and even a faulty theorem, which he corrected by giving a formal proof. ...
Gergely's user avatar
  • 267
12 votes
3 answers
433 views

Why are impredicative constructions used less in type theory than in material set theory?

Many infinitary objects in (say) ZFC are constructed with impredicative principles. The natural numbers are formed by intersecting every inductive set (whose existence is given by the axiom of ...
Trebor's user avatar
  • 3,688
20 votes
1 answer
284 views

Examples of formalisation of abelian categories

The question I would be interested to hear about examples of formalisation of the theory of abelian categories in theorem provers, and in particular formalisations of things like the zig-zag lemma and ...
Kevin Buzzard's user avatar
5 votes
0 answers
1k views

What's the general idea (intuition) behind Andrej's topos where reals are countable? [closed]

I am very surprised that Andrej Bauer claimed to have found a topos where reals are countable. He said it'll take a month to write down the proof, and I think that's very understandable. However, I'm ...
ice1000's user avatar
  • 5,877
14 votes
4 answers
305 views

Algorithms obtained through constructive formalization

Formal proofs in proof systems that avoid the law of the excluded middle and certain other principles can be automatically converted into algorithms. What useful new algorithms have been produced by ...
Will Sawin's user avatar
16 votes
1 answer
539 views

Proof assistants and formalised mathematics in the MSC database

I was looking at the MSC2020 database and I find it hard to identify a field suitable for works about proof assistants and formalised mathematics. 03B70 ("Logic in Computer Science") might ...
Filippo Alberto Edoardo's user avatar
22 votes
3 answers
410 views

To what extent is formalized mathematics publishable?

I am interested in contributing to the formalization of mathematics, but I don't know the extent to which such activities are publishable. Here are some questions in this vein: How can one determine ...
Dustin G. Mixon's user avatar
2 votes
2 answers
193 views

What is known about minimal sets of axioms? [closed]

There are several axioms that are known to be independent of the usual ones; for instance, the Axiom of Choice. This axiom can be stated in several equivalent ways, e.g.: For every set $A$, $\mathcal{...
wizzwizz4's user avatar
  • 495
8 votes
1 answer
120 views

Have the common algorithms in existing computer-assisted proofs been transitioned to proof assistants?

In my experience, one of the most common applications of computer-assisted proofs in math is establishing that a given system of constraints is infeasible. Here are some examples of settings and tools ...
Dustin G. Mixon's user avatar
21 votes
1 answer
469 views

How hard is computing integrals in Lean?

Are there tools in mathlib which let you give computations of integrals which would roughly follow standard methods for solving them? For now let me restrict attention to some undergrad-level ...
Wojowu's user avatar
  • 1,038
8 votes
1 answer
139 views

What are some useful resources for a mathematician interested in learning Isabelle/HOL?

What are some useful and reliable resources for a mathematician interested in learning Isabelle/HOL? Could be online (websites) or physical (books).
taylor.2317's user avatar
  • 1,308
13 votes
2 answers
177 views

verifying combinatorial constructions - choice of a proof assistant

The choice of the proof assistant to use for formalisation depends on the area quite a bit; e.g. they say that algebraic topology comes easy in HoTT assistants. What would be the most natural choices ...
Dima Pasechnik's user avatar
13 votes
1 answer
165 views

Representing $\Bbb RP^2$ in Lean: building a type representing a particular set

I need to work with the set of all lines in the Cartesian plane. For my context, the natural way to think of this is that a line can be described by an equation $Ax + By + C = 0$, where $A$ and $B$ ...
John's user avatar
  • 325
11 votes
2 answers
117 views

Proof assistants with dynamic scope/local instances/etc.?

Say I'm formalizing something in group theory, and I'm working with some action $\cdot$ of $(G, +)$ on a set. In my math textbook, the identity of $\cdot$ is explicitly mentioned once (if that), and ...
Joshua Grosso's user avatar
27 votes
8 answers
728 views

Where can I find lists of theorems that have been verified?

I recall many years ago seeing a very large and well-interlinked (by computer) list of verified results starting from base assumptions and leading to all sorts of things that naive me did not expect ...
25 votes
3 answers
343 views

Examples of new mathematics discovered through formalization?

In his essay Why formalize mathematics?, Patrick Massot discusses several reasons behind why a working mathematician might be interested in proof formalization. One of the the reasons he discusses is, ...
19 votes
0 answers
248 views

Can we automatically get around set-theoretic difficulties?

One of the main technical annoyances of working with (large) categories is the variety of set-theoretic difficulties that come about with it: if we use ZFC as background logic, then those large ...
Wojowu's user avatar
  • 1,038
26 votes
2 answers
952 views

What set-theoretic definitions can't easily be formalized in a type theory?

Most proof assistants (with some exceptions like Isabelle/ZF or the B method) rely on type theory. See also the MathOverflow question What makes dependent type theory more suitable than set theory for ...
ErikMD's user avatar
  • 407
46 votes
2 answers
1k views

Are some proof assistants better suited for given areas of math than others?

There are many different proof assistants out there, and I think it is reasonable to expect that more or less all results we prove in everyday mathematics can be proven in any of them. One nice way to ...
Wojowu's user avatar
  • 1,038
24 votes
2 answers
648 views

Why haven't all of the "hundred greatest theorems" been formalized yet?

The "hundred greatest theorems" used to be maintained here. See this page for the current status of the formalization of these theorems. Apparentely, Fermat's Last Theorem, the Isoperimetric ...
Dustin G. Mixon's user avatar
18 votes
2 answers
294 views

How can I prove facts about floating point calculations?

In computing, there is a standard called IEEE 754. Unlike in mathematics, computers have to fit numbers into a finite amount of space; to do this, they use a format a bit like scientific notation, ...
wizzwizz4's user avatar
  • 495
13 votes
1 answer
153 views

Exotic natural language summaries of formal proofs

Mathematical proofs written in natural language can often be used as guides to create formal proofs in proof assistants, depending on the level of detail of the proof and how many results and concepts ...
Will Sawin's user avatar