LeanCert for numerical log bounds (re: PNT#892, PNT#914)

Stream: PrimeNumberTheorem+

[Alejandro Radisic]

Following up on @Terence Tao comment on PNT#914 about whether LeanCert could streamline the numerical log evaluations in PNT#892:

Short answer: yes.

LeanCert's interval_decide tactic handles Real.log natively via verified Taylor series, so the manual bounds become one-liners.

a_bound, the three helper lemmas (log_five_bounds, log_three_lt, log_three_gt, 55 lines of manual Taylor series with geometric remainder bounding) are eliminated entirely:

-- Before: 55 lines of exp_bound', Finset.range, sum_le_tsum, geometric series
-- After: bounds inlined directly
theorem a_bound : a ∈ Set.Icc 0.92129 0.92130 := by
  norm_num [Chebyshev.a_simpl]
  constructor <;> nlinarith [Real.log_two_gt_d9, Real.log_two_lt_d9,
    (by interval_decide : 1.098612 < Real.log 3),
    (by interval_decide : Real.log 3 < 1.098613),
    (by interval_decide : 1.609437 < Real.log 5),
    (by interval_decide : Real.log 5 < 1.609438)]

psi_num: the log bounds for primes 7, 11, 13, 17, 19 (each 4 lines of log_lt_iff_lt_exp + exp_eq_tsum_div + Finset.range + norm_num) become:

have log7bound  : log 7  < 1.946 := by interval_decide
have log11bound : log 11 < 2.398 := by interval_decide
have : (log 13 < 2.57) ∧ (log 17 < 2.84) ∧ (log 19 < 2.95) :=
  ⟨by interval_decide, by interval_decide, by interval_decide⟩

Net effect: -77 lines, +14 lines. One tradeoff: psi_num needs maxHeartbeats 800000 (up from 400000) since interval_decide is doing more computation internally, it still builds in ~23s.

I have a branch that builds. Happy to PR if there's interest. Credit to ajirving for the actual psi_num proof; this just swaps the numerical plumbing for LeanCert's verified interval arithmetic.

[Terence Tao]

This looks good to me (and now the three have statements you listed in psi_num that can be combined into a single conjunction provable by split_ands <;> interval_decide). The additional heartbeats is a downside, but the increase in conceptual simplicity will be useful when generating variants of these sorts of arguments in the future, and hopefully we can move these sorts of computations into very stable files with minimal imports that rarely need to be rebuilt. (I am in fact thinking of reviving a centuries-old practice and creating log_tables.lean that does nothing but create high precision logarithms of the first few natural numbers.)

[Alejandro Radisic]

Could even be something like this with python, then interval_decide re-verifies :grinning_face_with_smiling_eyes:

import leancert as lc, math

x = lc.var('x')
cfg = lc.Config(taylor_depth=20)

for n in [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 30]:
    result = lc.find_bounds(lc.log(x), {'x': (n, n)}, config=cfg)
    lo = math.floor(result.min_lo * 1e6) / 1e6
    hi = math.ceil(result.max_hi * 1e6) / 1e6
    print(f"lemma log_{n}_gt : {lo} < log {n} := by interval_decide")
    print(f"lemma log_{n}_lt : log {n} < {hi} := by interval_decide")

With LogTables.lean imported, Chebyshev just references cached lemmas, the table builds in ~7s and rarely needs rebuilding

Let me know and I'll PR it

[Terence Tao]

This sounds good. Actually there are a few other minor places in the repo where numerical bounds on logs are used, e.g., https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/MediumPNT.lean#L783 https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/MediumPNT.lean#L795 https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/MediumPNT.lean#L1952 https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/BKLNW.lean#L194 . In these cases, the proofs are already quite short, but if there is some streamlined unified way to deal with these sorts of computations via a static LogTables.lean file that looks like a sustainable solution to me. (The cheap thing to do is simply to move each of these statements into a lemma in LogTables.lean and figure out how to organize that file later.)

[Terence Tao]

Someone just pointed out to me that the LeanCert code introduces a large number of additional axioms beyond the standard ones, e.g.,

'LogTables.log_2_gt' depends on axioms: [propext,
 Classical.choice,
 Lean.ofReduceBool,
 Lean.trustCompiler,
 Quot.sound,
 LeanCert.Core.gaussianSq_iteratedDeriv_bound,
 LeanCert.Core.iteratedDeriv_erfInner_zero_div_factorial,
 LeanCert.Core.IntervalRat.erfInner_contDiff,
 LeanCert.Core.IntervalRat.piRatLo_lt_pi,
 LeanCert.Core.IntervalRat.pi_lt_piRatHi]

What is the nature of these axioms? For these sorts of purely numerical and totally non-controversial calculations, dependence on external axioms is not an existential issue (and we will inevitably need to import some very large numerical calculations as axioms at some point), but it would be good to transparently disclose such dependencies whenever necessary.

[Kim Morrison]

These are just axiom statements in the LeanCert source code, e.g.

• https://github.com/alerad/leancert/blob/main/LeanCert/Core/IntervalRat/TrigReduced.lean#L54
• https://github.com/alerad/leancert/blob/main/LeanCert/Core/HermiteBounds.lean#L87
• https://github.com/alerad/leancert/blob/main/LeanCert/Core/IntervalRat/Taylor.lean#L2040

[Letter]

gaussianSq_iteratedDeriv_bound is False (AI-generated proof):

import LeanCert.Tactic.IntervalAuto

open LeanCert.Core
theorem gaussianSq_iteratedDeriv_bound_false : False := by
  let gaussianHalf (x : ℝ) : ℝ := Real.exp (-(x^2 / 2))
  have h_sq : iteratedDeriv 4 gaussianSq 0 = deriv^[4] gaussianSq 0 := by
    simpa using congrArg (fun g => g 0) (iteratedDeriv_eq_iterate (n := 4) (f := gaussianSq))
  have h_half : iteratedDeriv 4 gaussianHalf 0 = deriv^[4] gaussianHalf 0 :=
    congrArg (fun g => g 0) (iteratedDeriv_eq_iterate (n := 4) (f := gaussianHalf))
  have hcont : ContDiff ℝ (↑(4 : ℕ)) gaussianHalf := by fun_prop
  have hit : iteratedDeriv 4 gaussianSq 0 = (Real.sqrt 2) ^ 4 * iteratedDeriv 4 gaussianHalf 0 := by
    have hfun : gaussianSq = fun x => gaussianHalf (Real.sqrt 2 * x) := by
      funext x
      grind [gaussianSq]
    simp_all [iteratedDeriv_comp_const_mul]
  have hderiv4_sq : deriv^[4] gaussianSq 0 = (12 : ℝ) := by
    have : iteratedDeriv 4 gaussianSq 0 = (Real.sqrt 2 : ℝ) ^ 4 * (1 + 1 + 1) := by
      simpa [hit, h_half, show (-1 : ℝ) ^ 4 = 1 by norm_num] using
        Polynomial.deriv_gaussian_eq_hermite_mul_gaussian 4 0
    grind
  have : (12 : ℝ) ≤ 2 := by simpa [hderiv4_sq] using gaussianSq_iteratedDeriv_bound 4 0
  linarith [hderiv4_sq]

/--
info: 'gaussianSq_iteratedDeriv_bound_false' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 LeanCert.Core.gaussianSq_iteratedDeriv_bound]
-/
#guard_msgs in
#print axioms gaussianSq_iteratedDeriv_bound_false

[Johan Commelin]

Oof, that's not good. I think these axioms need to be very clearly communicated, and will need community vetting.
This is a strong signal that when combining AI with formalization, it is best to aim for axiom-free (aka only std 3 axioms).

[Kim Morrison]

Hooray for Lean clearly telling us what is broken. :-)

[Alejandro Radisic]

This indeed was critical.

Some LeanCert-specific placeholders had been introduced (including one false statement for a Gaussian derivative bound). Those placeholders leaked into downstream dependency traces (including logTables.log_2_gt), even for purely log-focused lemmas.

Fixed:

• Removed all five flagged axioms (gaussianSq_iteratedDeriv_bound, iteratedDeriv_erfInner_zero_div_factorial, erfInner_contDiff, piRatLo_lt_pi, pi_lt_piRatHi).
• Replaced pi bounds with fully proved lemmas.
• Removed the sinc high-derivative placeholder path.
• Removed the erf/Hermite placeholder path from the verified interval-eval route.
• The interval_decide path for log and trig is axiom-free and sorry-free. #print axioms on log table lemmas will show only standard foundations + Lean.trustCompiler / Lean.ofReduceBool.

Remaining:

• PNT repo is still pinned to an older LeanCert artifact/version. Will shortly update the tag and LeanCert version in PNT.
• Once dependency pin/manifest is updated to the fixed LeanCert revision, those LeanCert-specific axioms should disappear from #print axioms LogTables.log_2_gt.
• Remaining trust will be standard foundations plus native_decide compiler trust (Lean.trustCompiler / Lean.ofReduceBool), which is expected for reflected computation.

Conservative erf bounds:

• As part of removing unsound placeholders, erfPointComputable was switched to a fully sound sign-aware enclosure ([-1,0], [0,0], [0,1] depending on input sign), replacing the previous unsound Taylor-path dependency.
• Next step is restoring tight, fully proved erf enclosures (no axioms) via a stronger certified bound pipeline. I will work on this today and have it ready as soon as possible.

Will be submitting a PR to PNT with the updated LeanCert soon.

Sorry for the oversight, I really should have caught this before releasing.

[Sébastien Gouëzel]

Is there still the keyword axiom anywhere in your repository?

[Alejandro Radisic]

No axiom declarations remain (rg "^axiom\s+" is empty). There are sorry statements in Examples/ and one in Core/LogBounds.lean (monotonicity lemma). None are in the interval_decide evaluation path for log/trig.

Verified via #print axioms on the interval/log/trig core theorems (showing only standard foundations; plus compiler trust when reflected computation is involved)

[Matthew Ballard]

Despite all of us hitting issues with published research during work, I think most mathematicians haven’t viscerally endured the dangers of dependency management

[Alejandro Radisic]

Also added CI soundness guards to LeanCert: regex check for axiom declarations, sorry allowlist, and assert_no_sorry on all certified evaluation paths. This kind of regression can't happen again. The conservative erf enclosures have also been tightened.

[Sébastien Gouëzel]

It would be even better to remove all the sorry, except in test and example files.

[Alejandro Radisic]

Outside Examples/ and Test/, there are no actual sorry placeholders in LeanCert proofs as of now, I addressed the Core/LogBounds.lean one. The only non-example/test regex match is a documentation snippet in Tactic/Interval.lean (not compiled code, just a docstring, removing it now).

The allowlist is for Test/ and Examples/

[Terence Tao]

Matthew Ballard said:

Despite all of us hitting issues with published research during work, I think most mathematicians haven’t viscerally endured the dangers of dependency management

True, but at least with Lean dependencies that are of a propositional nature, one always has the option of replacing any result proven via an unsafe import with a sorry, thanks to propext, so it is relatively easy to amputate any bad import if need be. As long as the results proven by such imports are already known (or strongly believed) to be true by non-formalized means (e.g., non-rigorous numerical computation), the downside risk seems containable, and I am comfortable with using an experimental import to prove things like lemma log_2_lt : log 2 < 0.693148. (But the calculus would change of course if the import was for a foundational resource such as Mathlib.)

[Matthew Ballard]

I understand that reasoning but am perhaps less adventurous with general AI-generated imports running code on "my" machine for the relative gain.

[Terence Tao]

Beyond the introduction of new axioms, increased heartbeats needed to typecheck, and metaprogramming exploits (of the type that leanchecker etc. are supposed to guard against), what are the known exploits concerning importing malicious Lean files that one should be aware of?

[Matthew Ballard]

I am sure there are more exploits than I can think for the Lean code itself. But my main concern is running code from sources more generally these days.

[Terence Tao]

For non-formally verified code, sure, there are an infinite number of potential risks and exploits, but with Lean I would hope that one could actually enumerate all the possible exploits with a very finite list (well, I guess there are always undisclosed kernel-level exploits or something, but this seems like a very remote risk to me).

[Matthew Ballard]

I think there are two separate things here: soundness of a given theorem and arbitrary execution of code. In a non-adversarial situation, I don't worry about the latter nor the former. To guard against the latter, I run things in a VM but even then I am not eager to nuke it and rebuild the configuration.

[Matthew Ballard]

But this applies to anything I pull off github and most things off brew these days.

[Matthew Ballard]

Certainly not particular to Lean

[Terence Tao]

Oh, so can adding an external github repository to one's lake manifest result in arbitrary local execution of (non-Lean) code? That is indeed a significant security risk, and significantly weakens the entire promise of Lean as offering the ability to work with untrusted collaborators to supply code.

[Kevin Buzzard]

https://github.com/leanprover/lean3/issues/1781

[Matthew Ballard]

Lean provides the ability to trust mathematics (i.e., theorems proven) by unknown collaborators, but as it is also a (very flexible) general purpose programming language, executing unreviewed code from an unknown source is subject to all the usual security dangers that come with running code in any language. It should be noted that even opening a Lean file in VS Code is executing Lean code on your machine (because Lean is started when the file is opened).

More generally, you can have confidence in any formally verified theorems about code. But for something like here which is AI generated and calling Python in the background. It is not possible to verify its behavior completely.

[Terence Tao]

Hmm, so at present there is no technical way to implement something like the option 2 of the issue Kevin linked to, in which the imports one adds to the manifest are disallowed from making io calls, or are somehow restricted to a subset of Lean of the type generally used in mathematial proofs?

[Matthew Ballard]

Short of sandboxing your install in some way yourself. I don't know of such. But I might not have the most up to date info.

[Terence Tao]

This is actually rather concerning to me. If I understand this correctly, the entire lake manifest system is in fact a security vulnerability for anyone downloading a local version of the repository?

[Matthew Ballard]

Which repository?

[Terence Tao]

This repository (PNT+), which contains an entry for leancert in its lake-manifest.json. Are you saying that if leancert is somehow compromised to permit arbitrary code execution then PNT+ also becomes compromised?

[Jireh Loreaux]

I think there is a slight discrepancy here, if I understand your question correctly. The concern isn't so much that we're concerned about exploiting leancert (and then that being exploited in PNT+), but rather that the leancert code itself is the arbitrary code execution (which even calls out to Python if I understand correctly), and that this code is run in PNT+.

[Terence Tao]

I guess I need a quick primer on what lake manifest actually does. When one includes leancert in lake-manifest.json, does this mean that when one runs lake build or whatever, that all relevant Lean files in leancert are run, including potentially ones which make calls to external software tools that are to be run locally by the user?

[Terence Tao]

We also have a python script supplied by @Alejandro Radisic within PNT+ itself to auto-generate the LogTables.lean file, but this is not directly part of leancert which, as far as I understand, does not make any external Python calls (and given that the user building PNT+ may not have the same version of Python, or any Python at all, it seems it would be quite difficult to have any such external call successfully replicated on an arbitrary local build, without sophisticated malware programming).

[Mac Malone]

Yes, when lake build is run any modules from another package (e.g., leancert) that you use and import in yours will be built. Building said modules can result in them running arbitrary code. For example, if that code has #eval launchNukes, then said code would be run (just like it would be if it was in a file you were editing).

[Terence Tao]

This makes me significantly less enthusiastic about importing any experimental packages at all.

[Terence Tao]

Does this also mean that in the event that Mathlib itself is somehow compromised to include a malicious Lean file in their next version, that every single user of Mathlib could then have their devices vulnerable when they update Mathlib?

[Bryan Gin-ge Chen]

Yes, and that is something we are very aware of when reviewing PRs and working on mathlib CI.

[Matthew Ballard]

Yes, that applies to Mathlib too. But what is different about Mathlib is that I know the maintainers are very aware of the responsibility and potential dangers and take serious efforts against that

[Matthew Ballard]

The same goes for FRO and the core language itself

[Eric Vergo]

It's worth noting that this is the case for a lot of software (not just lean)

[Sebastian Ullrich]

Terence Tao said:

Are you saying that if leancert is somehow compromised to permit arbitrary code execution then PNT+ also becomes compromised?

No, not immediately. The commit reference stored in the manifest as a cryptographic hash makes sure of that. Only when running lake update could new malicious code be introduced, so the diff of the dependency should be as closely reviewed as accepting a PR changing the project's own code. But this really is true even outside of meta code if a dependency e.g. changes a def that some theorem's statement is based on.

[Matthew Coke]

https://cacm.acm.org/opinion/it-takes-a-village-to-teach-privacy/

[Terence Tao]

Is it technically feasible to create some sort of "safe" subset of Lean that is sharply more limited in what it can accomplish and execute, but still expressive enough to generate mathematical proofs, and which can be imported by a project in the full Lean language?

[Matthew Coke]

I'm in favor of creating a "safe" subset of Lean

[Johan Commelin]

I guess you would be looking for code that has access to some monads (like MetaM) but not others, like the IO monad.
But some part of the system will have to do IO stuff, when importing files. Not sure if/where the boundary could be placed.

[Sebastian Ullrich]

All the money behind the Java language was not able to make this airtight, as far as I know. This is an acknowledged attack vector behind the packaging systems of virtually any major language. I should also mention our new reference manual page https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-proofs that walks through all the levels of checking a Lean proof and what vectors they do and do not cover.

[Matthew Coke]

@Sebastian Ullrich it's a bit of a Project Hail Mary?..sorry, shameless movie plug

[Terence Tao]

Perhaps the standard root Lean file of a project would have access to IO etc. but would be a static file that verifies that all the other Lean files in the project only use whitelisted monads etc. and then imports them?

[Terence Tao]

Though I guess it would be infeasible to put all of Mathlib into the whitelisted subset of Lean, so one has to still accept Lean files that internally only use whitelisted operations but import Mathlib. Ugh, I see the problem with where to draw the boundary.

[Sebastian Ullrich]

I strongly believe that the OS level, rather than the language level, would be the only feasible isolation approach. Especially on Linux there are mature tools like bubblewrap and firejail that should be able to provide very high guarantees for e.g. lake build not touching anything outside .lake. I would be happy to see people experimenting with and sharing such setups for Lean projects.

[Matthew Ballard]

This is not user friendly but underlies what I use https://developer.apple.com/documentation/virtualization/running-linux-in-a-virtual-machine

[Jireh Loreaux]

Sebastian Ullrich said:

for e.g. lake build not touching anything outside .lake.

Indeed, but if you're working interactively with Lean in VS Code, then you would also need VS Code to be executed within a jail like this too.

[Matthew Ballard]

Can you get away with a remote codebase and a local VS Code? I don't use VS Code so am not sure.

[Jireh Loreaux]

I think you should be able to make this substitution in my claim and it is still valid: VS Code = any IDE that provides interaction with Lean via the LSP

[Jireh Loreaux]

Although I indeed don't know how sandboxed is the remote VS Code over ssh setup. I assume not very.

[Terence Tao]

I accept that OS-level security features are the strongest line of defense against these sorts of vulnerabilities. Still, I am not willing to give up entirely on the untrusted or semi-trusted import ecosystem, as it seems like a natural formal analogue of the existing mechanism of having one paper cite and rely upon a (partially trusted) paper in the literature (though with the additional complication that the cited paper can now potentially execute arbitrary code on one's local device).

Would it be possible to create a diagnostic tool that could scan a Lean repository and check that all of the Lean code in that repository contains only whitelisted operations (e.g., calls to Mathlib, no IO functions beyond import, etc.)? This might not catch all exploits, but could be an additional line of defense (especially against accidental vulnerabilities created by AI generated code, as opposed to exploits inserted by genuinely malicious agents).

[Johan Commelin]

@Terence Tao Just to confirm, are you trying to defend against:

1. untrusted code that makes you believe a theorem is true, even though there isn't actually a valid proof
2. untrusted code that uses your machine to mine bitcoin, and upload the contents of your hard drive to evil.underground.com

[J. J. Issai (project started by GRP)]

To add to this mix (or have someone move this message to a different channel), how bad are things on a) my system and b) the sandbox system if I do all of my work using live-lean.org (the web interface to lean, or sandbox as I call it)? Does any of the code I might unintentionally import reach out to files on my system? Assume I have no github repo and try to rely only on Mathlib and recommended packages.

[Terence Tao]

Johan Commelin said:

Terence Tao Just to confirm, are you trying to defend against:

1. untrusted code that makes you believe a theorem is true, even though there isn't actually a valid proof
2. untrusted code that uses your machine to mine bitcoin, and upload the contents of your hard drive to evil.underground.com

Closer to 2, but more precisely untrusted code written by an AI that unwittingly involves dangerous calls to external tools that might theoretically be used by a malicious third party to create an exploit, or at least modify the state of one’s computer in an unwanted fashion.

[Franz Huschenbeth]

Makes me wonder, if one day we may have a predicate isRestrictedToFolder, which proves that all IO Read / Write are restricted to this Folder and then we can AI-Hammer a proof in CI, whenever Dependencies update. But we are probably still a long way from such level of software verification.

Btw the terminology for such attacks is Supply Chain Attacks, the Javascript Package Registry NPM is hit like every month with a big attack. Lean probably has to little economic value at the moment to be a big target, but caution is always important.

[Matthew Ballard]

Personally, I am much more worried about AI that wittingly involves bad calls and is very good at hiding it from human eyes.

[Terence Tao]

Yes, so a tool that can pick up (at least some fraction of the time) such calls, somewhat similar to how #print axioms picked up the clandestine use of additional axioms, would be helpful, even though I acknowledge that such a tool may not detect sufficiently camouflaged calls.

[Franz Huschenbeth]

Terence Tao said:

Yes, so a tool that can pick up (at least some fraction of the time) such calls, somewhat similar to how #print axioms picked up the clandestine use of additional axioms, would be helpful, even though I acknowledge that such a tool may not detect sufficiently camouflaged calls.

So essentially a Anti Virus / Malware Detection Software for Lean Code. Maybe the Lean FRO, would sponsor such tool at some point. A open source tool might be too insecure in the sense, that we would have to trust the creators.

[Terence Tao]

Or maybe just a low-tech script that at least identifies all such external calls within the lean code. I would like to think that in any good-faith mathematical Lean package, 99% of the code is either routine statements, definitions, and proofs,plus maybe some metaprogramming of custom tactics, and only 1% would involve calls to external tools like Python or whatever, and perhaps this is a small enough rate that one can just rely on human review of that 1% to see if any red flags are present.

[Terence Tao]

Would it be fair to say that pretty much all potential exploits or security vulnerabilities from Lean imports not relating to soundness or excessive heartbeat consumption stem from using IO (e.g., to call external tools)?

[Marcelo Lynch]

Terence Tao said:

Would it be possible to create a diagnostic tool that could scan a Lean repository and check that all of the Lean code in that repository contains only whitelisted operations (e.g., calls to Mathlib, no IO functions beyond import, etc.)? This might not catch all exploits, but could be an additional line of defense (especially against accidental vulnerabilities created by AI generated code, as opposed to exploits inserted by genuinely malicious agents).

In the limit, it might be interesting to consider providing something like this with some digital signing scheme from within the ecosystem (e.g. reservoir?). Then we can verify before pulling the dependency that the commit is 'trusted' by that verification.

[David Michael Roberts]

Terence Tao said:

natural formal analogue of the existing mechanism of having one paper cite and rely upon a (partially trusted) paper in the literature (though with the additional complication that the cited paper can now potentially execute arbitrary code on one's local device).

How about a paper than can perform "arbitrary code injection" in the reader's brain, not just infect another paper with a malicious false result? :upside_down:

[Joachim Breitner]

Terence Tao schrieb:

Oh, so can adding an external github repository to one's lake manifest result in arbitrary local execution of (non-Lean) code? That is indeed a significant security risk, and significantly weakens the entire promise of Lean as offering the ability to work with untrusted collaborators to supply code.

To follow up on this, I added a (short) entry to our official FAQ:

Is it safe to build Lean code and libraries?

Lean is a general purpose programming language with rich compile-time features. Therefore building a Lean project, opening a Lean file or running commands like lake update can execute arbitrary code from the project or any of its dependencies. This “supply chain attack” vector exists in essentially all programming language ecosystems, including LaTeX. If you need to build code that may be actively malicious, do so in a properly isolated environment (e.g. a virtual machine).

I'm sorry that the world is as messy as it is, for now the most important thing is to avoid misconceptions.

[Alastair Irving]

The bounds in LogTables.lean look very useful for the explicit numerics we need, for example in the Chebyshev bounds, but I wonder if it would be better to revert the MediumPNT proof to the previous version rather than depending on LeanCert. The changes to MediumPNT>lean don't really shorten the proof and now MediumPNT depends on native_decide and can't be built until after LeanCert.

[Terence Tao]

Ah, good point, there is value in minimizing dependencies in some portions of the PNT+ project; already people are using results from PNT+ as axioms in other formalizations (e.g., of Erdos problems) and it would be nice if one could reduce the transitive dependencies. I've made a PR for this reversion now.

[(Tom de Groot) Tomodovodoo]

I agree with at least the minimalization of axioms in PNT+, though I think dependencies should be looked at in a per case basis at the very least.