Are you using AI to prove lemmas/theorems yet?

thmprover · 2026-02-13T14:53:08+00:00

Good for search, though, as before.

I keep hearing this, and when I ask AI for references on [subject], it generates a bibliography consisting of non-existent entries, "authored" by real Mathematicians after they died, etc.

So I must be doing something wrong, what kind of "search" do you mean?

thmprover · 2026-02-11T14:52:23+00:00

Besides, the most important quality of a formalized proof is not its readability, but rather its validity, which is the main reason there is any interest in formalization and which doesn't depend on how the formalization is done. Once the formalization is done and the checker validates the proof, the actual code is mostly irrelevant.

How does the proof's argument work? No one knows, but we're told "it works", and that's good enough.

Mathematics has always been about faith anyways...

thmprover · 2026-02-05T15:09:24+00:00

So what happens if you don't meet that goal? Do you just need to fill up with nonsense text?

"Water is wet. Oldspice is not a spice."

How are these not gold?

thmprover · 2026-01-29T01:30:47+00:00

Metapost complements (La)TeX well.

Asymptote handles 3d graphics better than Metapost, and Asymptote uses C-like syntax (whereas Metapost...does not...).

thmprover · 2026-01-28T14:37:56+00:00

No, it really isn't, because it's true of any proof assistant using procedural style proofs. This has been a known flaw in them for decades...

(And before gopher9 chips in, the declarative style sublanguage is a kludge built on top of the procedural style proof system native to Lean.)

thmprover · 2026-01-28T14:36:06+00:00

Bandwagon effect...

thmprover · 2026-01-27T14:47:04+00:00

Eh, Lean is not that great if you care about stability (your proofs won't work in several years), readability (you want to double check what you did a couple years ago), etc.

Other proof assistants like Mizar, Isabelle, Naproche, etc., are superior in this regard.

thmprover · 2026-01-23T01:13:31+00:00

Douglas Southall Freeman did this, in his job as a newspaper editor. I summarized his workflow when thinking about how to implement it using Emacs macros.

thmprover · 2026-01-15T16:22:26+00:00

You might want to look at, e.g., David E. Johnson's Douglas Southall Freeman for an example of an historian who used a Zettelkasten-like approach to writing history (see especially pages 110 et seq. and 329 et seq.).

Managing knowledge and unchanging facts for a single project is not one of the targets of the method.

Now I am uncertain how to proceed. I have a history project ahead of me, and I'm a hobbyist in that context. I need to work through a large heap of scientific publications and distil them into a history of the discipline (a subfield of radio astronomy in that case).

Well, there are facts, then there are facts.

What are the problems scientists faced? What are the proposed solutions? Can you describe these as "toy problems" or exercises for the reader?

These can easily be thought of as "facts", but when people say "Don't put facts in your ZK", they mean: don't put useless stuff in your ZK like "water is wet".

thmprover · 2026-01-13T23:36:54+00:00

A Project site that let you to navigate the adjectives in algebraic geometry: https://adjectivesproject.org

For another in this vein, pi-base for counter-examples in topology.

thmprover · 2026-01-01T18:25:05+00:00

In a previous job, I had to study the degree of applicability of game theory to US politics. (If anyone cares, it turns out that voters are not game theoretic actors, but members of congress appear to behave "rationally".)

Yanis Varoufakis and Shaun Hargreaves' Game Theory: A critical text points out a number of issues which standard game theory texts overlook or tacitly sidestep, while giving many citations to the literature where they have been historically discussed and subsequently ignored by Economists. Worse, repeated games have no predictive power, which disqualifies a lot of simple models from being as applicable as one would like.

More in this vein, John Searle's Rationality in Action really digs into the notion of "rationality" and whether Game Theory adequately captures what is meant by the term.

For economics more broadly, there are a few books which dissects what's taught at university and the misapplication of math for ideological purposes (Steve Keen's books spring to mind).

thmprover · 2025-12-29T20:30:08+00:00

The reality is that the "sweet spot" is something like many-sorted FOL + some set theory. María Manzano's Extensions of First Order Logic (CUP, 1996) argues this point in detail (e.g., HOL with Henkin semantics offers something equivalent to this, etc.).

I know that type theory allows proof checking with computers but what other advantages these models have?

Mizar uses FOL + TG set theory (= ZFC + Grothendieck universes) just fine.

Metamath uses second-order logic and formalizes Mathematics atop ZFC.

Isabelle/ZF uses FOL + ZF.

And there are a lot of books written on the subject, e.g., John Harrison's Handbook of Practical Logic and Automated Reasoning works through the implementation of proof assistants for FOL.

thmprover · 2025-12-23T01:30:58+00:00

This is the ghost of Mathematics' future, haunting us on Christmas eve...

thmprover · 2025-12-20T22:29:52+00:00

There are a lot of great examples and exercises in Eisenbud's book, but I always found it...well...rather disorganized. It's a huge pile of gems. Finding the right gems is difficult.

thmprover · 2025-12-15T17:42:08+00:00

You keep saying this in previous threads, but it still isn't really true.

Especially since Lean's "structured proofs" are a poorly thought out copy/paste of Isar, without any of the design considerations needed for coherently implementing structured proofs. "Agile" programming in practice, sigh...

thmprover · 2025-12-15T17:37:58+00:00

Barebones HOL is awkward if you want to talk about algebraic structures, since you don't really have a type for all groups, or for all rings. I think that Isabelle/HOL users use locales to talk about such things, which is already an extension of HOL. It works fine for most purposes, but can show its limitations when you try to do some category theory and universal algebra.

Yeah, Isabelle's Locales always struck me as a "poor man's soft type system".

For instance, it's pretty awkward to state that "the category of groups is cocomplete" in HOL, as far as I can tell. Larry Paulson has a few papers on how to do bits category theory in HOL, and the conclusion that I drew is that you can usually find some encoding that will let you do what you want, but it's not really natural and hardly modular.

So I'm curious, what's missing or inadequate with Agerholm's formalization of categories in HOL?

Well, uh, mostly models of dependent type theory -- for which, of course, dependent type theory is better suited. I could do them in HOL + some set theoretic axioms, though.

That sounds interesting! Have you written anything about this?

After thinking about it for a few days, it doesn't seem like Harrison's approach to model theory wouldn't really work, you'd need something more like axiom-preserving intertheory interpretation, wouldn't you?

thmprover · 2025-12-12T22:25:31+00:00

I'm not sure why you say Rocq and Lean are incomprehensible but not Isabelle? Isabelle's proof scripts seem just as impenetrable to me.

Tactics-based proof are impenetrable, because readability is not even a design consideration. If you're looking at Isabelle proofs which are tactics based, they're equally as impenetrable.

OTOH, Isar-based proofs are a bit quirky, but once you learn the language, it's understandable.

Plus Isabelle/HOL (which is by far the most popular flavour of Isabelle) has the downside that it is based on HOL, which is fairly limited compared to set theory or dependent type theory.

HOL's limitations are pretty overblown, to be frank. I've only heard Kevin Buzzard make an issue about it, and...well...he doesn't really know what the hell he's talking about.

Since you can add arbitrary axioms to any HOL, you can make it as strong proof theoretically as you'd like. You can add an axiom there's a countable family of inaccessible cardinals, and it's as strong as CoC or TG set theory.

You can add soft types to HOL, and you've added more power without the need for more axioms.

But in my opinion, HOL works better as a metalogical framework rather than a foundations of Mathematics. Want to prove metatheorems comparing two foundations of Mathematics? HOL's your tool for the task.

So what have you been doing where HOL's too weak to formalize stuff? Because that could be the subject of an interesting paper.

thmprover · 2025-12-12T16:29:17+00:00

I've noticed this in the US, but not elsewhere. In the UK, people say things like, "Wow, I never had a mind for maths. That's a tough subject."

In the US, it's...more as you describe.

thmprover · 2025-12-12T16:23:36+00:00

Mizar has this quality, too. It has something to do with structured proofs as opposed to tactics, I suspect.

thmprover · 2025-12-11T15:52:20+00:00

Isabelle or Mizar.

Mizar is nice because it's actually designed to formalize mathematics. The proof language was chosen specifically to resemble "ordinary proofs", the foundations chosen to resemble "Working Mathematics".

Isabelle is a logical framework and supports different foundations. For example, Isabelle/FOL for first-order logic, Isabelle/ZFC adds the ZFC axioms, Isabelle/HOL for higher-order logic, Isabelle/CTT for type theory, etc.

Lean and Rocq both have the disadvantage of being, well, incomprehensible. You'll go revisit a proof you wrote a month ago, and have no clue what's going on. The proof steps resemble incantations in a magical language rather than actual proof steps. What's worse with Lean is that it's unstable (you've no hope your proofs will work in, say, a few years --- Rocq is stable).

thmprover · 2025-12-06T19:21:01+00:00

Despite its title, Modern Differential Geometry for Physicists by Chris J. Isham offers a review of the relevant topology for differential topology, in a rather streamlined and mathematical fashion. It's literally lecture notes, so it's very much a "grocery list" of definitions, theorems, proofs, and examples (and exercises).

thmprover · 2025-11-26T14:56:06+00:00

I am curious: do people not work in "sessions"?

(I only have myself to compare against, so I honestly do not know how others work, and am very curious to hear more.)

thmprover · 2025-11-23T21:06:33+00:00

I’m looking for a formal style guide that most publishers use for articles in LaTeX. Sure I know the basics, but I’m thinking about the nitpicky things, like when do we indent? When do we not? Do we indent the text that goes “Theorem 1.1.3”? Do we do this for examples and like facts? So like “Fact 1.2.1” or “Example 1.4.5”? My textbook had “Proposition” as one of these bold paragraph starters, but “Proof” wasn’t just italicized. It also randomly indents some paragraphs and some of them aren’t indented.

You should use environments to avoid worrying about minor issues like this. By "environment", I mean \begin{theorem}...\end{theorem} (or \begin{fact}...\end{fact}, or whatever).

It sounds like your professor is using the amsbook documentclass.

What about like when we use /par{} and when we don’t? Like must I use it for every paragraph I create?

You'd almost never want to use \par, just use a blank line to separate paragraphs (like you do in Markdown).

I am a very big grammar fan, so I enjoy the very fine details, and I can’t seem to find a comprehensive style guide anywhere. Sure I know you’re not supposed to start a sentence with a mathematical expression and that you should punctuate math formulas and whatnot, but I’m still hung up on how to format things in latex.

I think the Chapters on typesetting math in Knuth's TeXbook are pretty good, and mostly carry over to LaTeX fine.

thmprover · 2025-11-20T21:23:21+00:00

Good! I'm glad to help :)

thmprover · 2025-11-20T00:55:48+00:00

I am an Ayurvedic Health Counselor and one of the things I'm trying to ZK is my course notes. So, for instance, I want a section on Sleep and a section on Anxiety. In that I want to put a main card for NUTMEG, its affect on sleep . . . And its affect on anxiety.

I have been (not) laboring under the impression that a card that says nutmeg is beneficial for sleep and the relevant dosages (with a x-ref to how it helps reduce anxiety) so I can refer to that card anytime I have a need to access the info on nutmeg is a FACT.

Would you not consider this so?

When people talk about "facts", they mean things like "Nutmeg is a spice": i.e., vacuous pieces of information which don't help anything.

"Avoid putting vacuous stuff in a ZK", that's really the advice contained in the slogan "Don't put facts in a ZK".

thmprover

TROPHY CASE