Terence Tao's personal log

Terence Tao's log on the Integrated Explicit Analytic Number Theory network project (IEANTN), which is being hosted within the PNT+ project. This log is inspired by a similar log for the Equational Theories Project.

Day 2 (Jan 16, 2026)

This project has been in development for several weeks, but was finally "officially launched" yesterday with my blog post announcement. If I had been a bit more organized, I would have started this log earlier to document the early stages of the project. Those stages can still be reconstructed from the discussion on the Lean Zulip channel, but going forward I will try to make a more organized recounting of events here.

Initially, the project started by focusing on two relatively easy "tertiary" subprojects:

The LCM project, to show that $\mathrm{LCM}(1,\dots,n)$ is not a highly abundant number for sufficiently large $n$, and specifically for $n \geq 89683^2$.
The Erdos 392 project, which aims to formalize a full solution to Erdos problem #392, which asserts that $n!$ can be factored into $n/2 - n/2\log n + o(n/\log n)$ pieces.

Thanks to a flood of contributions, both human and AI-generated, both projects are close to completion. The final LCM theorem is proven, conditional on one explicit prime number theorem of Dusart (which we would eventually plan to formalize, but this has not yet even been started), and one technical multiplicative number theory calculation that has been claimed but not yet completed.

While preparing this log I noticed something strange about the Erdos #392 project: in the dependency graph, the final theorems were not linked up to the rest of the proof! This was a misformalization issue that is now fixed; you can read more about it here. So there are a few more lemmas needed than I previously thought to finish off this subproject, but it is still largely completed.

Harald Helfgott has been contributing some further mini-projects to formalize. An identity relating the Mobius summatory function to the error term in the count of squarefree numbers is nearly done; only the final theorem remains to be proven, and this has already been claimed. A longer "appendix" on ways to estimate the Riemann zeta function is not quite as advanced, with roughly half of the sublemmas formalized so far, but it is proceeding nicely.

The most ambitious project currently is to formalize this paper of Fiori, Kadiri, and Swidninsky (FKS2), relating explicit prime number theorems for the Chebyshev function to explicit prime number theorems for the prime counting function. Here I am encounting the somewhat recursive nature of the literature here; there are facts from previous papers of Rosser-Schoenfeld and of Broadbent, Kadiri, Lumley, Ng, and Wilk (BKLNW) that this paper relies upon, and BKLNW in turn relies on past literature also. It may take some time to get to the bottom of all this!

Nevertheless, some lemmas are beginning to get formalized, and already a number of omitted positivity conditions, or "off by one" errors in summation ranges, have been identified by Pietro Monticone, Steven Rossi, and Aayush Rajasekaran. Hopefully these will not propagate to cause issues downstream.

Meanwhile, contributions are coming in to the older non-explicit side of the PNT+ project. Matteo Cipollina has just completed a formalization of the Hadamard factorization theorem and its specialization to the Riemann zeta function, which will certainly come in handy later in the explicit PNT+ project. We are also closing in on the prime number theorem in arithemtic progressions, with only a handful of lemmas needed to finish off this milestone! (On the other hand, the Chebotarev density theorem is still extremely far from completion; we barely have a viable roadmap to this theorem at present.)

Day 3 (Jan 17, 2026)

Lots of progress in various directions. The two misformalized final theorems in the Erdos project have now been formally proven again, thanks to Pietro Monticone and Aristotle. Alistair Irving noted that one of the outstanding tasks to prove (an identity for the prime counting function) was essentially already proven in a different component of the PNT+ project, leading to a one-line proof; this is a good example of the synergy I had hoped to see when hosting the IEANTN within the PNT+ project.

The LCM project relied on a single theorem of Dusart. I decided to go ahead and enter in all the other main results of Dusart's paper into the IEANTN as blueprinted, formalized statements of theorems (but with proofs omitted). Previously I had a somewhat complex workflow where I would use an LLM to extract LaTeX from a PDF of the paper, enter in the LaTeX as comments to the lean file, and then start entering in the blueprint metadata and the formalization; I have found that after doing this for one or two lemmas, Github Copilot "catches on" to what I am doing and offers increasingly longer and more accurate autocompletes. Today I discovered that I can skip one step by directly dumping in a cut-and-pasted version of the PDF text into the comments of the Lean file. The format of that cut-and-pasted document is quite ugly to human eyes, but apparently still very readable to LLMs, so this workflow worked very smoothly, with the main results of the paper all entered in about an hour (and near the end I it was almost just repeatedly pressing "Tab" to accept the autocomplete).

Harald Helfgott has pointed out the new TME-EMT wiki, which would be a prime source of further results to enter into the IEANTN as we continue scaling up the project.

The formalization process is picking up some gaps in the Mathlib literature, for instance the absence of an integration by parts lemma for the Stieltjes integral. There is some debate as to whether to avoid such issues by using more elementary proofs instead, but the tentative consensus is to use the opportunity to fill in the gaps in Mathlib even if this takes a little longer to accomplish within the project.

There is some "golfing" going on behind the scenes, such as reducing the imports needed for some Lean files in the project (by Tomodovodoo) or taking advantage of the latest Mathlib lemmas (by Alistair Irving). Such technical improvements are not flashy, but certainly very much appreciated, and likely will be crucial in keeping the project compilation times manageable as it scales up. There is some hope that AI tools can also help with "autogolfing", but such tools have not yet been widely deployed for this task.

While doing some updates for FKS2, I noted that this paper used a neat pair of inequalities

$$ \psi(x^{1/2}) + \psi(x^{1/3}) + \psi(x^{1/7}) \leq \psi(x) - \vartheta(x) \leq \psi(x^{1/2}) + \psi(x^{1/3}) + \psi(x^{1/5})$$

due to Costa Pereira, so I created a (hopefully) quick subproject to formalize these.

A small technical note: I discovered that if a Lean file is not imported as a lean module to the blueprint file, then it is not picked up in the blueprint. I discovered this when the LCM project was reporting a suspicious amount of dark green (indicating provability without prerequisites), when in fact it relies on the aforementioned estimates of Dusart which have not yet been proven.

Day 4 (Jan 18, 2026)

An issue that shows up in formalization projects is how best to "spell" a given mathematical statement; there can be several options to express the same statement in Lean, but some may be more convenient than others.

An example we recently encountered involved the basic identity $$\psi(x) = \sum_n \theta(x^{1/n})$$ relating the two Chebyshev functions $\psi, \theta$ to each other, which is the basic input to the Costa Pereira inequalities. This identity is simple enough to state and prove, but one has to decide exactly what range $n$ should be. One option is to take an infinite sum over all $n \geq 1$, and note somewhere that the summand vanishes for all $n > \log x / \log 2$. The approach taken in Mathlib is to work with the finite range $1 \leq n \leq \lfloor \log x / \log 2 \rfloor$. This avoids the subtleties of manipulating infinite series, however the specific finite range $\lfloor \log x / \log 2 \rfloor$ can be inconvenient to work with. A possible compromise is to work with the range $1 \leq n \leq N$ for an unspecified "sufficiently large" $N$ and use the Mathlib support for filters to manage the "sufficiently large". Hopefully, the process of formalizing the Costa Pereira inequalities will reveal what choice of spelling is best.

The use of the autocomplete function of Github Copilot dramatically increases the speed of converting an informal LaTeX document (or PDF) into a LaTeX/Lean blueprint; but it comes at the cost of some inaccuracy in the conversion process. Recently it turned out that some formulae that had been commented out in the source LaTeX had been accidentally reproduced in the Lean text of the formalization of the corresponding lemma. Fortunately, this was caught by the human formalizer (Steven Rossi), and in any event would have been detected through the inability to formalize the current version of the lemma as stated in Lean. These multiple layers of verification help prevent the issue of AI-generated errors from propagating to unacceptable levels.

I discovered today that the FKS2 paper uses results from yet another explicit analytic number theory paper, namely that of Buthe. Fortunately, I was planning to formalize this paper anyway, and with the Copilot workflow it was not difficult to at least formalize the statements of the main results.

There is some discussion on the Zulip about how to implement integration by parts at low regularity (where the functions involved only are known to be of bounded variation), which we will need to estimate some Fourier transforms of some piecewise continuous functions. Aristotle seems to struggle somewhat with these analysis type problems, so we will likely have to first find a human-generated proof, but we are first looking through Mathlib to see if other analysis or measure theory tools can be of use.

Day 5 (Jan 19, 2026)

Project leaderboard: Unclaimed 32, Claimed 13, In progress 3, In review 1, Completed 49.

The Equational Theories Project log maintained, for some time, a "dashboard" of metrics tracking the progress of the project. So I decided to maintain a similar dashboard for this log, using the raw task counts for the Github project as a very crude metric of progress. This metric is imperfect in many ways - tasks vary widely in size, and a small number are purely administrative tasks (such as to test out some features of the project management system) - but will still hopefully give some coarse-scale impression of the size and rate of progress of the project.

Over at the Erdos problem web site, Thomas Bloom has proposed that once the IEANTN matures, it could play a role in hosting some sort of "competition" involving both humans and AI to improve various numerical constants in explicit analytic number theory. This seems like an excellent idea, particularly if we coordinate with the new TME-EMT wiki for such estimates. It will be several months at least before we will be ready to implement this, but I will keep the idea on my radar screen.

I finished inputting the informal proofs from the FKS2 paper into the project. With AI tools this was not too difficult (these tools were particularly helpful for inputting in the lengthy tables in the paper). These are particularly computationally intensive proofs, and it will be a challenge to convert them into formal proofs, but we will cross that bridge when we come to it.

The LCM project is essentially done, with the final PR coming in this evening. This concludes the proof of the least common multiple result assuming a prime number theorem of Dusart. The students that I am supervising now plan to refactor this proof to make a much more explicit pipeline between the input estimate and the output estimate, so that other prime number theorems than Dusart's can be entered in. A reasonable first goal here is to input other prime number theorems in short intervals (such as the ones listed here) and see what one gets out of that. (With the aid of Github Copilot, it was an easy matter to transcribe the results from that wiki into the project.)

Day 6 (Jan 20, 2026)

Project leaderboard: Unclaimed 39, Claimed 10, In progress 2, In review 7, Completed 53.

The LCM project is officially completed, with a completely formalized proof, starting from the prime number theorem of Dusart, that $\mathrm{LCM}(1,\dots,n)$ is not highly abundant for all $n \geq 89683^2$. My students will now try to refactor this proof to make it easy to explore alternate inputs, for instance what can be said assuming the Riemann hypothesis.

We've encountered some issues in the Costa Pereira subproject due to some infinite sums being accidentally written to be over the reals instead of the natural numbers, but this is in the process of being sorted out.

A very minor milestone: Yongxi Lin found the first (very small) actual error has been found in one of the papers we are formalizing, namely that an inequality is stated to be strict but is only proven to be non-strict. This is an insubstantial error - almost on the level of a typo - but is a small demonstration of what formalization of a published result brings to the table.

One of the great benefits of the structure of a modern formalization project, with its decomposition into many small and loosely interacting pieces, is that these pieces can be worked on asynchronously, by different collaborators, in a non-linear order. However, sometimes this advantage breaks down. In the Costa Pereira project, Morten Ness discovered an "off by one" formalization error in one of the sublemmas: an infinite sum was supposed cover the range $\sum_{k=1}^\infty$, but covered the range $\sum_{k=0}^\infty$ instead. (In Lean, natural numbers start at $0$.) Morten was able to fix the immediate sublemma at hand (basically by replacing k with k.succ), but by this point several downstream lemmas involving manipulations of these series had already been proven with the wrong range of k. Pietro Monticone was able to update all of these proofs with the new indexing, but it was more complicated than a simple search and replace. The lesson to draw here is that when a statement of a sublemma to prove depends in an essential way on several prior lemmas that have not yet been proven, the statement may be unstable enough that it may be a good idea to not prioritize the proof of that sublemma (unless the proof is simple or likely to be robust with respect to such changes).

Day 7 (Jan 21, 2026)

Project leaderboard: Unclaimed 35, Claimed 10, In progress 1, In review 6, Completed 59.

Harald Helfgott is closing in on a possible way to handle integration by parts for bounded variation functions; there is a proof of this by Wheeden and Zygmund that Aristotle looks capable of formalizing, though the proofs are not at Mathlib's level of quality so some intermediate process of creating a proof and then refining it within PNT+ may be needed. Other results in Wheeden and Zygmund, such as Fejér's theorem on pointwise convergence of Fourier series, have already been formalized by this approach, which bodes well.

Pietro Monticone also used Aristotle to automatically pick up a several typos in one of the results I had recorded in the repository: a prime number theorem of Johnston and Yang was claimed to hold for all $x \geq 2$, but this is false, and on inspection of the source material we found that it was in fact $x \geq 23$. A bit more seriously, I had a stated a number of prime number theorems to the effect that intervals such as $(x(1-\varepsilon), x]$ contained a prime for various values of $x$ and $\varepsilon$. However, the definition in the repository of HasPrimeInInterval requires one to specify the left endpoint and the length of the interval, whereas I accidentally specified the left and right endpoints, with the effect that these theorems were instead asserting the far weaker statement that the interval $(x(1-\varepsilon), x(1-\varepsilon)+x]$ contained an interval, which Aristotle rapidly found to be a consequence of Bertrand's postulate. This is now being fixed, but it demonstrates that automated tools can actually help reduce misformalization, and not simply to increase it.

Aristotle also found ways to derive many of the weaker, older prime number theorems recorded on in the repository as consequences of the stronger, newer ones in the repository. I could block this from happening by ensuring that the prime number theorems are imported in completely chronological order, but having the "cheap" proofs of these older results is a useful placeholder to have, as it is unlikely we will get around to formalizing the proofs of these older results for quite some time. But it is still worth making a note that the proofs are shortcuts rather than reflecting the historical proof of these results.

Finally, Pietro Monticone and Aristotle managed to completely finish off the Costa Pereira project now that all the misformalizations were fixed, completing the four remaining lemmas; this was not expected to be that difficult of a subproject, but it is still impressive to see how far automated tools have come in this regard. It does mean though that we might be running a little low on outstanding tasks, and I will have to add a few more to the queue soon!

Yongxi Lin encountered our first truly computation-intensive proof, requiring 100000000 heartbeats due to 120 separate applications of nlinarith. This will not be sustainable in the long term, so we will need to figure out more efficient ways to do these sorts of computations.

While trying to continue blueprinting the BKLNW paper I have realized that I have misunderstood the flow of logic in this paper. Like many other conventionally written papers, the main theorems of this paper are stated in the introduction, but are proven later in the paper, and in some cases the proof is postponed to appendices. On the other hand, some of the theorems stated in the introduction are used to prove lemmas later in the paper, which are then used to prove other theorems stated in the introduction. Because of this, extracting a linear ordering of the results in the paper is not entirely trivial, and the ordering I had chosen was actually rather incorrect, requiring a large permutation of the theorems in the Lean file to fix (among other things, the $k=0$ and $k \neq 0$ cases of the main theorem, Theorem 1, cannot be placed close together, because the $k=0$ case, together with a large number of further lemmas, are needed to prove the $k \neq 0$ case). Furthermore, I had collected a lot of the hypotheses used in various lemmas in a single Inputs structure for more convenient handling of these hypotheses, but I have now discovered that some of the hypotheses currently placed in Inputs are in fact proven in the paper using other hypotheses in Inputs, which defeats the purpose of having a unified Inputs structure in the first place, and this structure will now need to be broken up. This is all doable (perhaps with the aid of a large blackboard to diagram the logic of the paper), but requires all current contributionsn on BKLNW to be completed (and no further ones to be initiated). Perhaps the lesson to draw here is that one has to diagram the logic of a paper first before beginning the blueprinting process; proceeding linearly through the paper and blueprinting one section at a time can lead to awkward refactorings later due to the fact that the paper one is blueprinting is unlikely to be written in a purely linear order.

Day 8 (Jan 22, 2026)

Project leaderboard: Unclaimed 33, Claimed 11, In progress 1, In review 4, Completed 64.

Lawrence Wu has resolved yesterday's issue of a computational proof absorbing way too many heartbeats, by manually making an educated guess as to how a simplified proof would work, writing a skeleton for that guess in Lean, and then letting autoformalization tools do the rest. A nice showcase of the ability to resolve problems by a collaboration between multiple human participants and AI tools.

Pietro Monticone, using Aristotle, has discovered a minor error in the description of an old prime number theorem of Schoenfeld (see Theorem 12) in the new TME-EMT wiki (which I had used as a reference for the IEANTN). The theorem asserts that "the open interval $(x,x+x/16597)$ contains a prime for all $x \geq 2010759.9$", but it was incorrectly recorded as "$(x(1-1/16597), x]$ contains a prime for all $x \geq 2010760$". The difference between the two statements is very slight, but the latter turns out to be false (Aristotle found the counterexample $x = 2010880$). Because the precise constants in an explicit analytic number theory estimate propagate into other constants and numerics in the explicit analytic number theory literature, it is important to fix these minor numerical errors, so already the IEANTN project is paying dividends! (I have contacted the maintainers of the TME-EMT wiki to fix this issue.)

Some further errors, this time my fault, have been discovered by the same process: I had omitted some key factors of $\log x$ from some statements concerning primes in short intervals, and more subtly, when formalizing the logarithmic integral $\mathrm{li}(x) = \int_0^x \frac{dt}{\log t}$, I did not realize that the integral was singular at $t=1$ and that the integral needed to be interpreted in a principal value sense. These formalizations are now fixed, though at some point we will need to formalize some lemmas about this principal value integral in order to relate it to the easier to manage $\mathrm{Li}(x) = \int_2^x \frac{dt}{\log t}$.

I think I have a way forward on the BKLNW refactoring. Much of the problem stems from the appendix to that paper, whose main purpose is to generate a key estimate $|\psi(x) - x| \leq \varepsilon(b) x$ for $x \geq e^b$ that is used as input for the main body of the paper, but which itself requires many inputs from other papers. Because I was using a single Inputs structure to hold the inputs for both the main body and for the appendix, this led to the illogical situation in which the appendix results were using one component of Inputs to generate another, which made the entire design choice to route everything through a single Inputs structure pointless and confusing. My solution is to create a new Lean file just for the appendix, with its own namespace and own Inputs structure. There are still some other issues in the main BKLNW paper that will require a bit of refactoring, but I have formalized the appendix first, while the existing BKLNW tasks are resolving.

Day 9 (Jan 23, 2026)

Project leaderboard: Unclaimed 37, Claimed 11, In progress 1, In review 0, Completed 68.

jdominpa has found a possible minor error in the FKS2 paper, in that a hypothesis $B \geq \max(3/2, 1 + C^2/16R)$ will need to be augmented with an additional constraint $B > C^2/8R$. In applications where the constants do not need to be explicit, this type of issue is negligible, but unfortunately for this project it is important to get all the constants exactly right, so I contacted the authors, who confirmed the issue and the fix. Pietro Monticone has picked up a few other minor typos in the paper (mostly to do with writing non-strict inequality when strict inequality was intended, or vice versa).

Yongxi Lin has [finished off] the proof of Mertens' second theorem $\sum_{p \leq x} 1/p = \log\log x + B + o(1)$! This will hopefully be useful for some non-explicit analytic number theory applications. Mertens' first theorem should soon fall as well.

I've figured out a way to formalize the estimation of the logarithmic integral that will make for a small mini-project. Kevin Buzzard points out that one could circumvent this whole issue by artificially redefining the log integral $\mathrm{li}(x)$ as $\mathrm{Li}(x) + 1.0451$, which would technically work but feels wrong somehow (especially since this version of the integral will be inaccurate by a small roundoff error). On the other hand, in the Mertens' project above, Yongxi Lin made a redefinition of the Meissel-Mertens constant that deviated significantly in appearance from the textbook definition, but was a more practical starting point (and was proven equal to the textbook definition after a few lemmas). So there is a case for using non-traditional definitions of terms, but perhaps only when they provably coincide exactly with the standard definition.

Day 10 (Jan 24, 2026)

Project leaderboard: Unclaimed 43, Claimed 9, In progress 1, In review 2, Completed 69.

I wrote a brief post on the Zulip to summarize the progress so far.

Another very minor typo in FKS2 picked up by jdominpa; the condition $x_0 \geq 2$ is needed to prove (30), and hence also Theorem 3, although in practice this condition is always going to be satisfied, so this is unlikely to cause major issues. The Lean formalization exercise forces this sort of excessive pedantry, but this is the price one pays for getting an absolute guarantee of correctness.

Performed a refactoring of the FKS2 blueprint to organize the results in a more logical order; will do the same for BKLNW next. There are a few people who had claimed some tasks relating to the refactored files, but I am hoping that the disruption will be manageable.

Yongxi Lin has now also formalized Mertens' first theorem, as well as a related integral identity that will be useful later when improving the error term in these inequalities.

Day 11 (Jan 25, 2026)

Project leaderboard: Unclaimed 36, Claimed 10, In progress 0, In review 5, Completed 74.

Alejandro Radisic has used the recent Lean package LeanCert to establish some rigorous upper and lower bounds on $\mathrm{li}(2)$, namely $1.039 \leq \mathrm{li}(2) \leq 1.06$ (the true value is $\approx 1.0451$. But this will be the first time we are using an external import for this project, and so we are starting a discussion to see if there will be any technical issues in adopting this.

Finally managed to refactor BKLNW in a logical fashion. I had been tripped up by an apparent circularity: in the paper, Theorem 1 is used to prove Corollary 2.1, which is used to prove Corollary 5.1, which is used to prove Corollary 8.1, which is used to prove Theorem 1! But eventually I worked out what is going on: Theorem 1 has two parts (a k=0 part and a k>0 part), and the first instance of Theorem 1 in the above chain refers to the first part, while the second instance refers to the second part. Splitting the theorem into two separate subtheorems and placing them at very different locations on the blueprint resolves the issue.

One technical speedbump I encountered was that the CI check was reporting blueprint latex errors. Sometimes the error message lets one clearly locate what the error is and where it is located, allowing for easy fixes, but there was one mysterious error about "missing $ inserted" that stumped me for a while. Eventually, I had to build the blueprint locally (using lake build :blueprint) and compile the resulting blueprint (in .lake/build/blueprint, using xelatex since pdflatex for some reason doesn't like some of the blueprint LaTeX features) to find the error; even with this I had to start commenting out some code until I finally localized the issue to having LaTeX in section headers. I'm recording this issue here in case I (or anyone else) encounters something similar in the future.

Day 12 (Jan 26, 2026)

Project leaderboard: Unclaimed 34, Claimed 10, In progress 1, In review 4, Completed 81.

We are now entering the more computational side of the FKS2/BKLNW papers for the first time, in particular trying to formalize the fact that a certain estimate holds for all parameter choices in a table with about 25 rows in it. We have formalized the numerical property that these rows need to satisfy, and a proof that the first row obeys these properties, but doing the latter verification 24 more times would be tedious (though hopefully straightforward for modern AI tools). Recompiling these 25 proofs every time the files are updated could be noticeably problematic, so I plan to refactor all the computational component of the table to a separate standalone Lean file that only needs to be compiled once (at least until Mathlib updates). This will hopefully serve as a template for how to handle the many other tables in these papers.

Day 13 (Jan 27, 2026)

Project leaderboard: Unclaimed 34, Claimed 9, In progress 0, In review 1, Completed 89.

Getting close to being able to adopt LeanCert to solve numerical verifications (starting with the numerical estimation of li(2)). The plan is to keep all the theoretical components of the verification within the main blueprint system, and have a dedicated file to do the purely numerical component using LeanCert as an import. However, we are double checking that importing LeanCert will not impact the mathlib caching system, which is essential to keep mathlib updates possible within a reasonable time.

The tables are refactored in a similar way. One speedbump is that a key table (Table 8) in BKLNW turned out to have two versions: a short version appearing in the published paper, and an extended paper with many more rows. It is the extended table which is needed to verify other calculations. So the BKLNW table file now has both tables, and an outstanding task to verify that the short version is weaker than the longer one.

The formalization process has picked up a number of misformalizations in the project. Some new instances of an older misformalization, in which one mistakenly summed over the integers rather than the natural numbers, was picked up by Pietro with Aristotle. Pietro and Aristotle also picked up a numerical typo in the formalization of the first row of Table 8. Amusingly, while most of this table was AI generated, the issue was precisely the lack of AI use: I had typed in the first row by hand and then used Github Copilot to fill in the other 50 or so entries, but I forgot a digit in my row. Copilot did correct transcribe all the other rows though!

We have just discovered a potential major roadblock in the entire project. It appears that at least some of the key papers we are formalizing compiled their numerical tables using non-rigorous floating point arithmetic rather than rigorous interval arithmetic. As a consequence, many of the numerical constants appearing in the paper are untrustworthy in their final digit. For any practical application this is a negligible problem, but for formalization it is a real headache. Every numerical bound in the paper, e.g., eps < 0.5364, is now not actually the formal statement we need to formalize into Lean; we need something like eps < 0.5365 instead. But because there are long chains of dependencies between constants, it is not completely obvious how to round up each constant in the chain.

I have been adopting a "top down" approach to formalization in which I started with a very recent paper FKS2 and started formalizing it, recursively creating formalization projects for any reference used non-trivially by this paper as needed (e.g., BKLNW). But these roundoff errors have exposed a weakness to this strategy - if some constant in a paper five citations deep needs to be adjusted in the final digit, this can propagate all the way back up the citation chain requiring all sorts of small modifications to formal proofs. If we had robust pipelines in place then this might not be a problem, and the plan is to actually have such pipelines anyway, so maybe this will not be a problem. The other alternative is to flip to a bottom up approach in which we start formalizing only those papers without significant dependencies. That would be safer from the formalization project side, but less interesting from the pipeline side, because then we would have no examples of proofs with nontrivial inputs to experiment with.

Day 14 (Jan 28, 2026)

Project leaderboard: Unclaimed 31, Claimed 13, In progress 1, In review 1, Completed 89.

A test project by Harald Helfgott to formalize an identity involving the error term in the Mobius prime number theorem has now been completed thanks to the work of many contributors, with the final step finished off by Steven Rossi.

To deal with the rounding issues it looks like the simplest fix is to pad all numerical constants in various paper with safety margins, e.g., multiplying them by 1.01 or 1.001, with the multiplier increasing as one goes up the dependency chain of constants. So the final results may now be weaker by a percentage point or so from what is in print, especially if there is a long chain of dependencies, but hopefully once we have an integrated network in place these safety margins can be optimized away.

Separately in the PNT+ project (largely outside of the IEANTN, but sharing the same infrastructure), Alex Kontorovich and his team at Rutgers are launching a project to begin formalizing the well-known text of Iwaniec and Kowalski. Getting the whole text formalized sounds ambitious, but perhaps some significant portion is within reach now. Separately, the last remaining part of the Strong PNT project is in the process of getting properly blueprinted. (A full proof of the final theorem was achieved separately by Morph Inc., but it did not quite follow the blueprint we had, and it is non-trivial to integrate that proof into our repository.)

Day 15 (Jan 29, 2026)

Project leaderboard: Unclaimed 30, Claimed 14, In progress 0, In review 1, Completed 92.

Build times for the LeanCert li(2) verification exceed an hour on slow machines, so we are converging on a compromise: the lengthy numerical verification will be formalized in a Lean file, but this Lean file will be disconnected from the main project and so will not be forced to be built by default.

Day 16 (Jan 30, 2026)

Project leaderboard: Unclaimed 30, Claimed 14, In progress 0, In review 1, Completed 92.

Day 17 (Jan 31, 2026)

Project leaderboard: Unclaimed 30, Claimed 14, In progress 0, In review 1, Completed 92.

Progress on my end was held up for a day or so due to some technical mathlib local build issues, but with help from other project contributors I managed to resolve the problem. I have now been able to implement the safety margin idea mentioned previously; if it works for the test set of tables, then it will hopefully be a model for other numerical components of the project.

LeanCert is now merged into our project; we will see if any significant performance issues arise.

Started a new miniproject to formalize the classical Chebyshev estimates, which could serve as a substitute for a slightly weaker estimate of Rosser and Schoenfeld that is used in the literature. This is a large number of small tasks which should be suitable for beginners.

Day 18 (Feb 1, 2026)

Project leaderboard: Unclaimed 37, Claimed 16, In progress 0, In review 3, Completed 95.

I am realizing that the Chebyshev project will require a numerical verification of $\psi(x) \leq 1.11 x$ for all small $x$; with some AI assistance I realized that the original bounds would require verification up to around $x \leq 10^6$, but with some ad hoc optimizations I could get it down to more like $x \leq 10^5$. Still, this might be a little tricky to do natively in Lean. It will be interesting to see how that develops.

Formalizing that the tables in BKLNW are compatible with each other has proven to be surprisingly slow, even with safety margins implemented, due to various typos entered in when transcribing the tables using a mix of manual and AI autocompleted text. It appears that spot checks of AI-autocompleted tables is not fully reliable. Still, the errors are relatively easy to catch, check, and fix, so this should only be a short-term problem.

Pietro Monticone is doing automated runs of Aristotle on the project which is picking up any number of misformalizations, for instance here a typo in a definition of a quantity $a_2$ was picked up because a numerical table of values for $a_2$ was incorrect.

Day 19 (Feb 2, 2026)

Project leaderboard: Unclaimed 34, Claimed 13, In progress 0, In review 1, Completed 106.

A large fraction of the Chebyshev tasks are in fact already formalized now, thanks to the quick work of Pietro Monticone and Alistair Irving (and also Aristotle, although here many of the proofs are actually manually written). Some of the lemmas that I had anticipated to be extremely lengthy case checks ended up being quite straightforward after using powerful Lean tactics such as omega, which is I guess part of why we have these tactics in the first place.

Day 20 (Feb 3, 2026)

Project leaderboard: Unclaimed 28, Claimed 14, In progress 0, In review 3, Completed 109.

Harald Helfgott has started formalizing several key theorems from Wheeden-Zygmund and Montgomery-Vaughan in Lean, such as integration by parts for the Riemann-Stieltjes integral. He and I had some discussion on how best to document these formalizations and integrate them with the rest of the project.

Day 21 (Feb 4, 2026)

Project leaderboard: Unclaimed 28, Claimed 14, In progress 0, In review 1, Completed 111.

A technical issue with the Mathlib docgen CI has prevented us from building the blueprint (or anything else in the repository) for a few days, but Aayush Rajasekaran has implemented a workaround (basically by downgrading docgen-action).

I've started a new subproject, to formalize the estimates of Chirre-Helfgott, which can control the Chebyhshev function via Fourier analysis (and numerical verification of the Riemann hypothesis). This will eventually link up with the existing FKS2/BKLNW formalization, although this may take a while.

Day 22 (Feb 5, 2026)

Project leaderboard: Unclaimed 30, Claimed 20, In progress 0, In review 1, Completed 111.

Day 23 (Feb 6, 2026)

Project leaderboard: Unclaimed 28, Claimed 19, In progress 0, In review 3, Completed 112.

The work we have put in on Chebyshev bounds and on the least common multiple of $1,\dots,n$ has had an unexpected payoff: an unrelated project requires an upper bound on $L_n = \mathrm{lcm}(1,\dots,n)$, which we have almost already achieved in the project, except that we are missing a basic identity $\log L_n = \psi(n)$ which I will shortly create tasks to establish.

Day 24 (Feb 7, 2026)

Project leaderboard: Unclaimed 28, Claimed 18, In progress 0, In review 2, Completed 114.

Day 25 (Feb 8, 2026)

Project leaderboard: Unclaimed 28, Claimed 17, In progress 0, In review 3, Completed 114.

I have done some refactoring, moving some common definitions to a single file at the start of the project dependency tree, and also started integrating some numerical results of e Silva, Herzog, and Pardi. The blueprint docgen is still having issues, but is temporarily fixed, allowing me to create some new issues. In particular, a new miniproject has been launched, to derive the prime number theorem in short intervals of Dusart (used in the LCM subproject) as a consequence of some general implications, a prime number theorem with classical error term, a table of record prime gaps, and some brute force computation.

After some discussions with Alejandro Radisic it looks like we may be reviving the archaic practice of compiling logarithm tables, now as a verified Lean file, that is intended to be built once and then referred to as a stable import. UPDATE: Alejandro has in fact completed this refactoring already!

Day 26 (Feb 9, 2026)

Project leaderboard: Unclaimed 36, Claimed 21, In progress 0, In review 2, Completed 117.

An issue came up with the LeanCert import, in that it was discovered that it introduced several non-standard axioms, at least one of which was actually false. Alejandro has already addressed these issues, but it spawned a further discussion about the risks of dependency on experimental imports. For the current use case (to formally verify numerical inequalities, such as those required for building logarithm tables), the downside risk of soundness bugs seems acceptable to me, since one always has the option of replacing the imports by sorrys instead (assuming the imports are purely of a propositional nature, so one can use propositional extensionality).

However, the risk of security vulnerabilities due to the ability of Lean imports to run external code on the local machine building the import is a non-trivial concern. Several options were discussed on how to limit, or at least detect, such external code calls, which could for instance theoretically be an unintended component of AI-generated code, but it appears there are no good solutions to this problem at present, and so some review and trust of the import and its maintainance procedures is still needed, despite the abilities of Lean to guarantee soundness.

Day 27 (Feb 10, 2026)

Project leaderboard: Unclaimed 31, Claimed 21, In progress 0, In review 3, Completed 121.

Day 28 (Feb 11, 2026)

Project leaderboard: Unclaimed 30, Claimed 22, In progress 0, In review 3, Completed 121.

Day 29 (Feb 12, 2026)

Project leaderboard: Unclaimed 30, Claimed 27, In progress 0, In review 2, Completed 123.

Alejandro Radisic pointed out a subtle issue with the formalization of the prime gap tables of e Silva, Herzog, and Pardi, which among other things contains a list of record prime gaps amongst the primes up to $4 \times 10^{18}$. I had formalized the statement that every entry in this table corresponds to a record prime gap, but I neglected to also formalize the converse statement that every record prime gap up to $4 \times 10^{18}$ also appears in this table. Like Sherlock Holmes' "dog that did not not bark in the night", the absences in the table are at least as informative as the entries, and in fact for a later application it was the absence of unusually large gaps which was important. I am now adding in these converse claims, and also adding some consequences of these claims (in particular, an upper bound on the prime gaps up to $4 \times 10^{18}$ as "unit tests".

Day 30 (Feb 13, 2026)

Project leaderboard: Unclaimed 39, Claimed 25, In progress 0, In review 2, Completed 125.

Day 31 (Feb 14, 2026)

Project leaderboard: Unclaimed 32, Claimed 31, In progress 0, In review 2, Completed 126.

Pietro has used Aristotle once again to point out several misformalizations, arising from typos, and confusion between positive integers and natural numbers. In particular a large table of prime gaps that we were intending to use as an axiom was technically incomplete because (as stated) it did not address gaps of length zero. This would have been bad for the project as we would be importing a false axiom, which of course can imply anything! Fortunately we had a unit test in place to test that table up to primes of size 30, and by disproving that version of the claim, the misformalization was discovered. So the unit test was working exactly as intended.

Launched a few small tertiary subprojects. One is to formalize the standard argument that bootstraps numerical verification of the even Goldbach conjecture to numerical verification of the odd Goldbach conjecture via primes in short intervals. Another (currently work in progress) is to formalize the verification of Ramanujan's inequality for large $x$ from prime number theorems with a good error term.

Day 32 (Feb 15, 2026)

Project leaderboard: Unclaimed 33, Claimed 27, In progress 1, In review 5, Completed 133.

The Goldbach subproject is rapidly being formalized, with many contributions by Aaron Lin in particular, who also noted a very slight error in the verification of the odd Goldbach conjecture by Ramare and Saouter in 2003: they claimed to verify the conjecture up to $113256 \times 10^{17}$, but on formalizing the proof Aaron found out that they actually only verified up to the very slightly smaller $11325599999999886744004$. This has no actual impact since these results have since been superseded in multiple ways (most obviously by Helfgott's full resolution of the odd Goldbach conjecture), and it is not too difficult to do a bit more computation to extend Ramare and Saouter's work back to the original claim (this was done, with different numerical constants, by Kadiri and Lumley a bit later), but it does show that formalization can pick up these sorts of very minor issues in the literature. (Aaron also pointed out a silly misformalization of mine in the odd and even Goldbach conjectures, namely that I actually forgot to specify the restriction to odd and even numbers respectively.)

Alistair Irving pointed out that it is not necessary for some of the key results in PNT+, such as the medium prime number theorem, to be dependent on LeanCert (which in turn depends on native_decide), and that reducing the dependencies could be valuable for downstream projects that use various components of the PNT+ in their own formalizations. I have therefore reverted the small number of code changes in which we were using the log tables to verify various simple numerical inequalities, and instead use more ad hoc appeals to various Mathlib lemmas.

The Ramanujan project is now live, adding a large number of further small tasks to the project.

Day 33 (Feb 16, 2026)

Project leaderboard: Unclaimed 39, Claimed 36, In progress 0, In review 3, Completed 138.

Day 34 (Feb 17, 2026)

Project leaderboard: Unclaimed 37, Claimed 36, In progress 0, In review 1, Completed 144.

There is some interesting discussion on the Goldbach thread about how feasible it would be to actually formalize in Lean a computational statement needed in the proof of the odd Goldbach conjecture, namely that $[N, N + 4 \times 10^{18}]$ contains a prime for all $1 \leq N \leq 10^{30}$ (the upper bound for $N$ is somewhat negotiable). One approach here is to create a "ladder" of about $10^{12}$ primes that touch each of these intervals, but while such a ladder can be precomputed, its size is prohibitive. But it seems that verified primality testing in Lean is fast enough that such a verified computation might actually be within reach.

Day 35 (Feb 18, 2026)

Project leaderboard: Unclaimed 36, Claimed 32, In progress 0, In review 2, Completed 146.

Li Xuanji started a discussion on alternate ways to generate the log tables, leading to some interesting pointers to rapidly convergent series for the log and exponential functions.

Day 36 (Feb 19, 2026)

Project leaderboard: Unclaimed 34, Claimed 35, In progress 0, In review 4, Completed 146.

Day 37 (Feb 20, 2026)

Project leaderboard: Unclaimed 31, Claimed 35, In progress 0, In review 5, Completed 148.

Day 38 (Feb 21, 2026)

Project leaderboard: Unclaimed 31, Claimed 34, In progress 0, In review 6, Completed 148.

Day 39 (Feb 22, 2026)

Project leaderboard: Unclaimed 29, Claimed 35, In progress 0, In review 5, Completed 151.

Thanks to a rather heroic effort by Alex Kontorovich, the formalization of the solution to Erdos 392 is now complete! Here was a situation where two major AI tools (Claude and GPT) both struggled, ultimately due to some misformalizations and typos in the blueprint and Lean file that required expert human intervention. (See also Alex's social media post on his experience.)

Day 40 (Feb 23, 2026)

Project leaderboard: Unclaimed 29, Claimed 33, In progress 0, In review 5, Completed 153.

Day 41 (Feb 24, 2026)

Project leaderboard: Unclaimed 24, Claimed 32, In progress 1, In review 7, Completed 156.

Day 42 (Feb 25, 2026)

Project leaderboard: Unclaimed 24, Claimed 32, In progress 0, In review 5, Completed 159.

Day 43 (Feb 26, 2026)

Project leaderboard: Unclaimed 23, Claimed 28, In progress 2, In review 2, Completed 165.

Day 44 (Feb 27, 2026)

Project leaderboard: Unclaimed 23, Claimed 27, In progress 2, In review 2, Completed 166.

Day 45 (Feb 28, 2026)

Project leaderboard: Unclaimed 21, Claimed 28, In progress 2, In review 2, Completed 167.

The section on Chebyshev's estimates is now fully formalized, thus for instance we have formalized the theorem that $\psi(x) \leq 1.11 x$ for all $x>0$.

Day 45 (Mar 1, 2026)

Project leaderboard: Unclaimed 18, Claimed 28, In progress 2, In review 1, Completed 171.

Making a push now to formalize more of the Chirre-Helfgott paper. Helfgott has supplied an alternate version of the Fourier-analytic considerations in Section 4.1 that is self-contained, and hopefully easier to formalize.

Day 46 (Mar 2, 2026)

Project leaderboard: Unclaimed 37, Claimed 28, In progress 2, In review 2, Completed 172.

Day 47 (Mar 3, 2026)

Project leaderboard: Unclaimed 37, Claimed 29, In progress 2, In review 2, Completed 173.

Hyunsik Chae (and Codex) identified multiple small but non-trivial errors in the final stages of the Ramanujan project, such as claiming an upper bound of $0$ when instead it should be $\log x$. Part of the confusion stemmed from the fact that the source material consisted of combining two papers: a paper of Dudek and Platt involving two parameters $M_a, m_a$ that were constant, and a later paper of Platt and Trudgian adapting the argument to the case where $M_a, m_a$ now depended on a parameter $x$. I had taken some of the lemmas of Dudek and Platt and formalized them to handle this more general setting, but there were subtle errors in that manual translation that were only detected when an AI started computing the numbers properly and found discrepancies. In the end, we located the error and fixed it by [asking a further AI] to verify the computations in the original (natural language) papers, which we could cross-check against what a separate AI was doing for the Lean code. (In retrospect, we should have given both the natural language paper and the Lean code to a single AI and see if it could work out the issue by itself, but the above improvised workflow was satgisfactory, and also allowed the humans involved to understand the issue better.)

The Lean fix involved changing certain constants to functions. Perhaps this change could also have been done by AI, but I found it instructive to do it manually, making a change of definition in one line and then going to the five or six later lines of code that stopped typechecking, and fixing them as needed. This exercise helped me understand the logical structure of both the informal and formal argument; and as I have previously found, it is far easier to tweak a previously working piece of Lean code to do something slightly different than it is to write that code from scratch. So perhaps it makes sense to use AI tools mostly to get the initial working draft of code, but still perform "golfing" and other updates by hand, in order to maintain an accurate understanding of the code structure.

Day 48 (Mar 4, 2026)

Project leaderboard: Unclaimed 37, Claimed 29, In progress 2, In review 2, Completed 173.

Day 49 (Mar 5, 2026)

Project leaderboard: Unclaimed 36, Claimed 27, In progress 2, In review 1, Completed 176.

Day 50 (Mar 5, 2026)

Project leaderboard: Unclaimed 37, Claimed 27, In progress 2, In review 1, Completed 177.

Day 51 (Mar 6, 2026)

Project leaderboard: Unclaimed 36, Claimed 26, In progress 2, In review 2, Completed 177.

Another, potentially more serious issue found in the Ramanujan project: the arguments implicitly assume that a certain quantity $m_a$ is non-negative, but we need to apply it in a case where it is negative. This is likely fixable, but with some non-trivial changes to the argument, and I have contacted the authors about this.

Day 52 (Mar 7, 2026)

Project leaderboard: Unclaimed 35, Claimed 26, In progress 2, In review 1, Completed 178.

Day 53 (Mar 8, 2026)

Project leaderboard: Unclaimed 35, Claimed 26, In progress 2, In review 1, Completed 178.

Day 54 (Mar 9, 2026)

Project leaderboard: Unclaimed 35, Claimed 25, In progress 2, In review 1, Completed 179.

Day 55 (Mar 10, 2026)

Project leaderboard: Unclaimed 35, Claimed 23, In progress 2, In review 3, Completed 179.

Day 56 (Mar 11, 2026)

Project leaderboard: Unclaimed 35, Claimed 23, In progress 2, In review 3, Completed 179.

Day 57 (Mar 12, 2026)

Project leaderboard: Unclaimed 35, Claimed 23, In progress 2, In review 1, Completed 181.

Heard back from the authors of the source papers for the Ramanujan paper acknowledging the sign issue, but there should be a repair that does not dramatically alter the structure of the argument. However, some of the theorems in the current blueprint are already claimed by various contributors, so they will need to be notified if the theorem statements change. Hyunsik Chae has already gotten to work implementing such a fix.

One of the theorems in that project, pi_bound_2, had an incorrect reference in the source material (it pointed to one paper by Buthe instead of another), and as such was not previously assigned as a task, but I have now chased down the references and added enough theorems from the second paper of Buthe that this result should now be conditionally formalizable within the project.

Day 58 (Mar 13, 2026)

Project leaderboard: Unclaimed 38, Claimed 21, In progress 2, In review 1, Completed 182.

Progress is being made on correcting the Ramanujan file, though it has meant that some previously claimed tasks had to become unclaimed.

Pietro Monticone and the new version of Aristotle has been able to close a number of extant sorries, including some involving primality checking of very large numbers which was done by native_decide. Similarly to how we already implemented a log table file, we will now also implement a prime table file to store these large prime numbers for future use, in the hope that the verification of their primality only has to be done very infrequently.

Day 59 (Mar 14, 2026)

Project leaderboard: Unclaimed 34, Claimed 20, In progress 2, In review 3, Completed 185.

I have created a new file TMEEMT.lean to formalize the statements of the results in the TME-EMT wiki. With the aid of an AI agent, this was quite smooth, with three sections of the first chapter of the wiki formalized in a couple hours; in fact the main difficulty was in transferring over the bibliographic references, which I did not automate (there were enough edge cases with references that were difficult to source that I preferred to do that by hand).

Pietro and Aristotle managed to prove a Lean theorem that required verifying that two 18-digit numbers were prime, purely by native_decide! It turns out that the Decidable instance of Nat.Prime implements trial division up to the square root, which can be reasonably implemented at this size, though it takes about six minutes or so. As with the log tables before them, these numbers are being placed into a PrimeTables file for now. Perhaps in the future we will find faster ways to verify these sorts of large prime numbers.

Day 60 (Mar 15, 2026)

Project leaderboard: Unclaimed 33, Claimed 21, In progress 2, In review 1, Completed 187.

Day 61 (Mar 16, 2026)

Project leaderboard: Unclaimed 33, Claimed 21, In progress 2, In review 1, Completed 187.

Day 62 (Mar 17, 2026)

Project leaderboard: Unclaimed 33, Claimed 21, In progress 2, In review 1, Completed 187.

Day 63 (Mar 18, 2026)

Project leaderboard: Unclaimed 33, Claimed 21, In progress 2, In review 1, Completed 187.

Day 64 (Mar 19, 2026)

Project leaderboard: Unclaimed 33, Claimed 21, In progress 2, In review 1, Completed 187.

Day 65 (Mar 20, 2026)

Project leaderboard: Unclaimed 31, Claimed 21, In progress 2, In review 1, Completed 189.

Day 66 (Mar 21, 2026)

Project leaderboard: Unclaimed 31, Claimed 21, In progress 2, In review 1, Completed 189.

Day 67 (Mar 22, 2026)

Project leaderboard: Unclaimed 30, Claimed 22, In progress 2, In review 1, Completed 189.

Day 68 (Mar 23, 2026)

Project leaderboard: Unclaimed 30, Claimed 22, In progress 2, In review 1, Completed 189.

Day 69 (Mar 24, 2026)

Project leaderboard: Unclaimed 30, Claimed 22, In progress 2, In review 1, Completed 189.

Day 70 (Mar 25, 2026)

Project leaderboard: Unclaimed 30, Claimed 22, In progress 2, In review 1, Completed 189.

Day 71 (Mar 26, 2026)

Project leaderboard: Unclaimed 30, Claimed 22, In progress 0, In review 1, Completed 191.

Not much to report on the IEANTN side - UCLA is on a spring break - but the Iwaniec-Kowalski project is moving forward, with several backlog pull requests cleared and new blueprinting planned.

Day 72 (Mar 27, 2026)

Project leaderboard: Unclaimed 28, Claimed 23, In progress 0, In review 2, Completed 191.

Day 73 (Mar 28, 2026)

Project leaderboard: Unclaimed 27, Claimed 23, In progress 0, In review 2, Completed 192.

Xianji Li has found and implemented a nice way to approximate $\mathrm{li}(2)$ (or more generally any other logarithmic integral) to high accuracy, by first developing a highly convergent series for the logarithmic integral involving the Euler-Mascheroni constant, and also finding a highly convergent series for the latter.

Day 74 (Mar 29, 2026)

Project leaderboard: Unclaimed 27, Claimed 23, In progress 1, In review 1, Completed 192.

Day 75 (Mar 30, 2026)

Project leaderboard: Unclaimed 38, Claimed 23, In progress 0, In review 1, Completed 193.

Now that spring break has concluded, I am returning to a more active role in the IEANTN project, starting with fleshing out a few more tasks to be completed on the CH2 track. I am beginning to find a way to use AI tools and agents to partially automate this work, though I am still wary of automating beyond my ability to review changes. The first step is to obtain usable LaTeX versions of the argument to be formalized, either from the source files or by feeding a PDF (if this is all I have availabe) to an AI. Pasting that as commentary to the Lean file, I have found good success with Github Copilot in autocompleting most of the boilerplate LeanArchitect headers, as well as the formal statement of the theorem to be proved, especially once a significant number of prior such boilerplate already exists in the currently open files, although there are still complex cases (often involving the need to introduce auxiliary definitions or lemmas, or splitting up a single lemma into multiple components) that require manual attention. (In the case of splitting a lemma up into components, I often have to do the first component by hand, but then later components can be mostly autocompleted, especially if they are similar to the previous components.) Finally, I am getting an AI agent, armed with a markdown file built up from past experiences, to automatically catch formatting issues that were picked up by CI, which is beginning to close the somewhat painful iteration loop of having to wait for about half an hour for the repository CI to report whether the blueprint compiled properly. (I do have some ability to compile the blueprint locally with lake build :blueprint, followed by manually compiling the blueprint LaTeX file thus produced, but that still takes about ten minutes, whereas agents can do their proofreading in a minute or so.)

Day 76 (Mar 31, 2026)

Project leaderboard: Unclaimed 37, Claimed 22, In progress 1, In review 1, Completed 194.

Day 77 (Apr 1, 2026)

Project leaderboard: Unclaimed 39, Claimed 25, In progress 0, In review 2, Completed 196.

Day 78 (Apr 2, 2026)

Project leaderboard: Unclaimed 38, Claimed 25, In progress 0, In review 1, Completed 198.

Day 79 (Apr 3, 2026)

Project leaderboard: Unclaimed 36, Claimed 26, In progress 0, In review 1, Completed 198.

Day 80 (Apr 4, 2026)

Project leaderboard: Unclaimed 36, Claimed 26, In progress 0, In review 1, Completed 199.

Day 81 (Apr 5, 2026)

Project leaderboard: Unclaimed 36, Claimed 26, In progress 0, In review 1, Completed 199.

Day 82 (Apr 6, 2026)

Project leaderboard: Unclaimed 52, Claimed 23, In progress 0, In review 1, Completed 199.

Starting to become more active on the project again; making a push now to formalize BKLNW (adding a dozen more tasks), and also to finish off the Ramanujan subproject (which meant that some stale claims needed to be unclaimed). So the dashboard will be somewhat fluid for a while.

Day 83 (Apr 7, 2026)