List of noncomputables

Stream: general

[Vasilii Nesterov]

Hi! While working on my formalization project I faced the following problem, which I don't know how to solve in Lean naturally.

I need to construct a counterexample which is a set of complex number of some form (linear combinations of square roots of integers over ℚ) satisfying a certain predicate isGood : ℂ → Prop. I have a tactic which proves isGood z for any number z in this form if isGood z is true. This set is large and (on paper) can be constructed by

1. Constructing a List C of candidates.
2. Filtering elements which satisfy isGood.
3. Use the filtered list with proofs of isGood to prove the desirable property of the set.

The problem is that these numbers are noncomputable and I can't extract "good" numbers after step 2.

The second problem is that I don't know how to apply a tactic "in runtime".

[Bjørn Kjos-Hanssen]

How about using a computable representation. For example
$\frac53\sqrt{-3}-\frac14\sqrt{2}$
could be represented as

![((5/3),-3),((-1/4),2)] : Fin 2 → ℚ×ℤ

[Vasilii Nesterov]

I tried to go it this way. In the construction, I need to use algebraic operations, so I have to implement all arithmetic for numbers of this kind and then prove that it lifts to ℂ. It feels like reinventing the wheel.

[Bjørn Kjos-Hanssen]

I guess the question is whether Mathlib has, e.g., $\mathbb Q(\sqrt 2)$ as a computable field.

[Kyle Miller]

Can you symbolically evaluate isGood? Could you share its definition?

[Kyle Miller]

The second problem is that I don't know how to apply a tactic "in runtime".

What's your definition of "in runtime"? Is it in the course of building a proof? Or do you have a compiled program that you want to run a tactic in?

[Vasilii Nesterov]

It's not the actual predicate I'm interested in, but let's suppose it's
isGood z := ||z|| = 1

[Kyle Miller]

Any reason you don't want to share the actual predicate you're interested in?

[Vasilii Nesterov]

By "in runtime" I mean that for example for this predicate norm_num could prove isGood z for any fixed z (if z is good of course), and I want to iterate through the list of numbers, for each of them trying to apply norm_num and filter those elements the tactic was successful with.

[Vasilii Nesterov]

Kyle Miller said:

Any reason you don't want to share the actual predicate you're interested in?

In my initial post I simplified the problem, putting unnecessary details aside. Actually, I am working with unit distance graphs on a plane to formalize the theorem stating that the plane is not 4-colorable. And isGood is
isGood u v := ||u - v||.

[Kyle Miller]

putting unnecessary details aside

Sometimes these things can be very dependent on details, so there's some risk in omitting them. It's also very useful having a #mwe of what you're working on, since answering your question with concrete code would involve someone answering to write a framework from scratch. (For example, without the #mwe I misread your question and didn't realize that you already had a tactic that can prove isGood z. But can it disprove isGood z as well?)

(Side note: I saw Aubrey de Grey give a talk at UC Berkeley about non-4-colorability. It's neat that you're formalizing this!)

[Kyle Miller]

There are a number of ways to evaluate tactics during the course of another tactic. Sometimes tactics expose a metaprogramming interface, but also you can invoke tactics via Syntax using docs#Lean.Elab.Tactic.evalTactic

[Mario Carneiro]

I remember someone at the ICERM22 meeting was pursuing a proof of the Hadwiger-Nelson problem for non-5-colorability (for which IIUC the current best result is 509 vertices). (Unfortunately I forget who it was, and I think it didn't progress much after that, it was a moonshot plan to begin with.) We talked a little about the proof strategy, and the points are all lying in a finite quadratic field extension, something like $\mathbb{Q}[\sqrt 2,\sqrt 3,\dots, \sqrt{17}]$, so formalizing this would probably mean developing computable arithmetic over this type to verify the graph and then reduce the rest to a SAT problem.

[Mario Carneiro]

For the Moser spindle, it seems like you can get away without doing any hard calculations: prove that you can make two diamond shapes, and use continuity to argue that there is an angle to put them at such that there is one additional unit edge

[Johan Commelin]

I think that was @Dustin Mixon at ICERM22

[Dustin Mixon]

Mario Carneiro said:

I remember someone at the ICERM22 meeting was pursuing a proof of the Hadwiger-Nelson problem for non-5-colorability (for which IIUC the current best result is 509 vertices). (Unfortunately I forget who it was, and I think it didn't progress much after that, it was a moonshot plan to begin with.) We talked a little about the proof strategy, and the points are all lying in a finite quadratic field extension, something like $\mathbb{Q}[\sqrt 2,\sqrt 3,\dots, \sqrt{17}]$, so formalizing this would probably mean developing computable arithmetic over this type to verify the graph and then reduce the rest to a SAT problem.

That's right. I didn't get very far with the project.

[Vasilii Nesterov]

All arithmetic in $\mathbb{Q}[\sqrt{2}​,\sqrt{3}​,\dots]$ is necessary only to construct the example. I found out that norm_num with a little extra effort can prove goals like $||u−v||=1$ when $u$ and $v$ are in this ring. It's the only fact about points in the example I have to prove. Then we can forget about complex numbers and work with general graphs. So, my question is: can we somehow avoid developing a theory about $\mathbb{Q}[\sqrt{2}​,\sqrt{3}​,\dots]$ by relying on norm_num?

[Kyle Miller]

If you can create an #mwe that reflects what you have set up and what you still want to do, maybe that's enough framework for it to be easy for someone to take a bit of time to fill in the meta code to drive norm_num?

[Vasilii Nesterov]

So, I have a tactic that can prove $||u - v|| = 1$ in all cases I care for constructing the example:

import Mathlib.Data.Complex.Basic
import Mathlib.Algebra.Squarefree.Basic
import Mathlib.Tactic

noncomputable def z1 : ℂ := 1/2 + Complex.I / 2 * √3

example : ‖z1^3 - z1^4‖ = 1 := by
  simp [z1, Complex.abs, Complex.normSq] -- with some additional simp lemmas
  repeat
    ring_nf
    norm_num [← Complex.ofReal_pow]

I'd like to:

1. Construct a list of complex numbers.
2. Iterate over pairs $(u, v)$ of its elements, trying to prove $||u - v|| = 1$ by the tactic above. If it succeeds add the corresponding edge (with the proof of $||u - v|| = 1$) to the graph.