The IBM mainframe that ran the calculations completing the proof of the four color theorem did not generate the proof. It simply executed the FORTRAN program that Haken and Appel (and Koch [1]) gave it.<\/p>\n
I don’t see the recent proof of finite-time blowup for solutions to the Navier-Stokes equations as entirely different. Computers did higher-level tasks for the OpenAI team than the mainframe did for Haken and Appel, and these tasks were not as directly programmed as the tasks that were given to the mainframe, but still machines do what they are told to do.<\/p>\n
Related posts<\/h2>\n\n- The seven color map theorem<\/a><\/li>\n
- Detecting errors with the four color theorem<\/a><\/li>\n<\/ul>\n
[1] John A. Koch was a programmer who worked on the four color proof with Haken and Appel. I don’t know how much credit he deserves, but I suspect it may be more than he was given.<\/p>\n","protected":false},"excerpt":{"rendered":"
The idea of using computers to assist with proofs is not new. The first major computer-assisted proof was published in 1976, the proof of the four color theorem by Kenneth Appel and Wolfgang Haken. The authors reduced the proof of the four color theorem to verifying calculations on 1,834 configurations, each checked by a computer […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[5],"tags":[],"class_list":["post-247877","post","type-post","status-publish","format-standard","hentry","category-computing"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"A 50-year-old computer-assisted proof","description":"Computer-assisted proofs are older than you may imagine. The first major theorem proved with the assistance of a computer was over 50 years ago.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/four-colors\/","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"A 50-year-old computer-assisted proof","og:description":"Computer-assisted proofs are older than you may imagine. The first major theorem proved with the assistance of a computer was over 50 years ago.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/four-colors\/","article:published_time":"2026-09-09T14:59:48+00:00","article:modified_time":"2026-09-09T14:59:48+00:00","twitter:card":"summary","twitter:title":"A 50-year-old computer-assisted proof","twitter:description":"Computer-assisted proofs are older than you may imagine. The first major theorem proved with the assistance of a computer was over 50 years ago.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247877","title":null,"description":"Computer-assisted proofs are older than you may imagine. The first major theorem proved with the assistance of a computer was over 50 years ago.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-09 14:24:10","updated":"2026-09-09 14:59:48","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"
\n\t\t\tHome<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tComputing<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tA 50-year-old computer-assisted proof\n\t\t<\/span><\/div>","aioseo_breadcrumb_json":[{"label":"Home","link":"https:\/\/www.johndcook.com\/blog"},{"label":"Computing","link":"https:\/\/www.johndcook.com\/blog\/category\/computing\/"},{"label":"A 50-year-old computer-assisted proof","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/four-colors\/"}],"_links":{"self":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247877","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/comments?post=247877"}],"version-history":[{"count":2,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247877\/revisions"}],"predecessor-version":[{"id":247879,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247877\/revisions\/247879"}],"wp:attachment":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/media?parent=247877"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/categories?post=247877"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/tags?post=247877"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}},{"id":247875,"date":"2026-09-09T09:17:20","date_gmt":"2026-09-09T14:17:20","guid":{"rendered":"https:\/\/www.johndcook.com\/blog\/?p=247875"},"modified":"2026-09-09T09:17:20","modified_gmt":"2026-09-09T14:17:20","slug":"ai-multiplier","status":"publish","type":"post","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/ai-multiplier\/","title":{"rendered":"AI is an intelligence multiplier"},"content":{"rendered":"A rising tide may lift all boats, but the AI tide lifts some boats much more than others.<\/p>\n
By all accounts, the best programmers have had the biggest productivity boost from AI. And top tier mathematicians are using AI to settle long-standing mathematical conjectures. AI is a powerful tool, but tools don’t come to life and make things on their own.<\/p>\n
I routinely have naive amateurs send me proofs of open conjectures, and naturally more recent such proofs involve AI. I’ll get an email saying something like “I’ve solved the Collatz conjecture using ChatGPT, but I’m not a mathematician so I need some help verifying the proof.” And of course the supposed proof is rubbish.<\/p>\n
The recent Navier-Stokes proof is impressive, but AI didn’t initiate the proof any more than LaTeX did. Nor did a child steer AI into proving the conjecture. Professional mathematicians were able to use AI to pursue their ideas at superhuman speed. But someone without an understanding of the Navier-Stokes problem, and familiarity with recent ideas for approaching the problem, could not have directed AI to produce a proof. <\/p>\n
Computer scientists have been saying “garbage in, garbage out” from the beginning. A variation on this aphorism for the age of AI would be “mediocrity in, mediocrity out.” <\/p>\n","protected":false},"excerpt":{"rendered":"
A rising tide may lift all boats, but the AI tide lifts some boats much more than others. By all accounts, the best programmers have had the biggest productivity boost from AI. And top tier mathematicians are using AI to settle long-standing mathematical conjectures. AI is a powerful tool, but tools don’t come to life […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[260],"tags":[],"class_list":["post-247875","post","type-post","status-publish","format-standard","hentry","category-ai"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"AI is an intelligence multiplier","description":"The most productive, most creative, and most intelligent people will benefit the most from AI.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/ai-multiplier\/","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"AI is an intelligence multiplier","og:description":"The most productive, most creative, and most intelligent people will benefit the most from AI.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/ai-multiplier\/","article:published_time":"2026-09-09T14:17:20+00:00","article:modified_time":"2026-09-09T14:17:20+00:00","twitter:card":"summary","twitter:title":"AI is an intelligence multiplier","twitter:description":"The most productive, most creative, and most intelligent people will benefit the most from AI.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247875","title":null,"description":"The most productive, most creative, and most intelligent people will benefit the most from AI.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-09 13:47:02","updated":"2026-09-09 14:17:21","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"
\n\t\t\tHome<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tAI<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tAI is an intelligence multiplier\n\t\t<\/span><\/div>","aioseo_breadcrumb_json":[{"label":"Home","link":"https:\/\/www.johndcook.com\/blog"},{"label":"AI","link":"https:\/\/www.johndcook.com\/blog\/category\/ai\/"},{"label":"AI is an intelligence multiplier","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/ai-multiplier\/"}],"_links":{"self":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247875","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/comments?post=247875"}],"version-history":[{"count":1,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247875\/revisions"}],"predecessor-version":[{"id":247876,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247875\/revisions\/247876"}],"wp:attachment":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/media?parent=247875"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/categories?post=247875"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/tags?post=247875"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}},{"id":247870,"date":"2026-09-09T07:43:36","date_gmt":"2026-09-09T12:43:36","guid":{"rendered":"https:\/\/www.johndcook.com\/blog\/?p=247870"},"modified":"2026-09-09T07:43:36","modified_gmt":"2026-09-09T12:43:36","slug":"formal-method-revolution","status":"publish","type":"post","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/formal-method-revolution\/","title":{"rendered":"The part of Navier-Stokes no one is talking about"},"content":{"rendered":"Yesterday OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics. The announcement has created a lot of buzz, as one would expect. But there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as their conventional human-readable proof.<\/p>\n
Quite a few other mathematical conjectures have been settled recently using AI, and these have also been accompanied with formal proofs, using Lean 4 in particular.<\/p>\n
Until very recently, generating machine-verifiable formal proofs has been excruciatingly tedious<\/strong>. In 2005, Henk Barendregt and Freek Wiedijk wrote<\/a><\/p>\nTo give an indication of how much work is needed for formalisation, we estimate that it takes approximately one work-week (five work-days of eight work-hours) to formalise one page from an undergraduate mathematics textbook.<\/p><\/blockquote>\n
That was the rule of thumb: forty hours per page<\/strong>. And this in the context of undergraduate textbooks. Research publications are much denser than textbooks. Furthermore, page 100 of a textbook probably depends mostly on material on pages 1 through 99. A sentence in a research article could cite anything that has been published before.<\/p>\nSay a research article takes 20 times more effort to formalize than page in an undergraduate textbook. Then formalizing the 166-page paper from OpenAI would take 132,800 person-hours. It took OpenAI 17 hours to verify their proof in Lean. I hesitate to use the word “revolutionary,” but lowering the cost of anything by four orders of magnitude<\/strong> is revolutionary.<\/p>\nI’ve used AI to generate formal proofs to check my work just for a little blog post. I wouldn’t dream of doing that if I had to pay someone a week’s salary to check my work.<\/p>\n
Formal verification doesn’t just apply to mathematics. You could, for example, formally verify that a set of security policies are consistent and that, given certain assumptions, they accomplish their purpose. You could formally verify that a smart contract imposes a certain maximum liability. You could verify the correctness of mission-critical algorithms. These problems are easier than formalizing mathematics research, and it is easier to quantify the return on investment.<\/p>\n
Related posts<\/h2>\n\n- Automation and validation<\/a><\/li>\n
- Formal methods let you explore the corners<\/a><\/li>\n
- When are formal methods worth the effort?<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"
Yesterday OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics. The announcement has created a lot of buzz, as one would expect. But there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[1],"tags":[324],"class_list":["post-247870","post","type-post","status-publish","format-standard","hentry","category-uncategorized","tag-formal-methods"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"The part of Navier-Stokes no one is talking about","description":"When OpenAI released their proof that solutions to the Navier-Stokes equations can blow up in finite time, they also released a formal proof in Lean 4.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/formal-method-revolution\/","robots":"max-image-preview:large","keywords":"formal methods","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"The part of Navier-Stokes no one is talking about","og:description":"When OpenAI released their proof that solutions to the Navier-Stokes equations can blow up in finite time, they also released a formal proof in Lean 4.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/formal-method-revolution\/","article:published_time":"2026-09-09T12:43:36+00:00","article:modified_time":"2026-09-09T12:43:36+00:00","twitter:card":"summary","twitter:title":"The part of Navier-Stokes no one is talking about","twitter:description":"When OpenAI released their proof that solutions to the Navier-Stokes equations can blow up in finite time, they also released a formal proof in Lean 4.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247870","title":null,"description":"When OpenAI released their proof that solutions to the Navier-Stokes equations can blow up in finite time, they also released a formal proof in Lean 4.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-09 11:31:29","updated":"2026-09-09 13:05:58","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"
\n\t\t\tHome<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tUncategorized<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tThe part of Navier-Stokes no one is talking about\n\t\t<\/span><\/div>","aioseo_breadcrumb_json":[{"label":"Home","link":"https:\/\/www.johndcook.com\/blog"},{"label":"Uncategorized","link":"https:\/\/www.johndcook.com\/blog\/category\/uncategorized\/"},{"label":"The part of Navier-Stokes no one is talking about","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/formal-method-revolution\/"}],"_links":{"self":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247870","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/comments?post=247870"}],"version-history":[{"count":4,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247870\/revisions"}],"predecessor-version":[{"id":247874,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247870\/revisions\/247874"}],"wp:attachment":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/media?parent=247870"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/categories?post=247870"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/tags?post=247870"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}},{"id":247864,"date":"2026-09-08T10:26:08","date_gmt":"2026-09-08T15:26:08","guid":{"rendered":"https:\/\/www.johndcook.com\/blog\/?p=247864"},"modified":"2026-09-08T12:48:11","modified_gmt":"2026-09-08T17:48:11","slug":"navier-stokes-in-the-news","status":"publish","type":"post","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/08\/navier-stokes-in-the-news\/","title":{"rendered":"Navier-Stokes in the news"},"content":{"rendered":"There are rumors that a long-standing math problem, one of the Millennium Prize problems, has been solved.<\/p>\n
The problem concerns technical properties of solutions to the Navier-Stokes equations<\/strong> [1], a set of equations that describe the dynamics of fluid flow. Popular accounts of the problem are often oversimplified and misleading.<\/p>\nSome reports will speak of the problem as “solving the Navier-Stokes equations.” The task is not to write down a closed-form solution, which can’t be done, or solve the equations numerically, which has been done for decades. The problem is to prove theoretical properties of solutions which are of little interest in practice.<\/p>\n
There has been progress toward settling the Navier-Stokes problem. Terence Tao wrote a post on this yesterday<\/a>.<\/p>\nWhat’s also\u00a0 interesting is the intrigue around the possible solution. A post<\/a> this morning says<\/p>\nIf I am reading this correctly, Tristan Buckmaster is alleging OAI has a resolution of Navier-Stokes \u2026 which maybe used info from Buckmaster and Levent Alp\u00f6ge\u2019s private Codex sessions.<\/p><\/blockquote>\n
Buckmaster asked OpenAI whether they used his private sessions and they have not responded. Update<\/strong>: Statement<\/a> from OpenAI.<\/p>\nPersonal note<\/h2>\n
This topic connects parts of my career spanning decades. My graduate work was in PDEs and I had some interest in the Navier-Stokes equations. Here are some notes<\/a> I wrote back in the day.<\/p>\nNow I work more with privacy than with PDEs. The question of whether OpenAI uses private data, contradicting their stated policy, is more relevant to my current work than whether the Navier-Stokes equations have global regular solutions.<\/p>\n
Related posts<\/h2>\n\n- Engineering a waterpark<\/a><\/li>\n
- Euler-Lagrange equations<\/a><\/li>\n
- Data privacy<\/a><\/li>\n<\/ul>\n
[1] I never know whether to say equation or equations. You’ll hear both. You could think of Navier-Stokes as one vector-valued PDE or three scalar-valued equations.<\/p>\n","protected":false},"excerpt":{"rendered":"
There are rumors that a long-standing math problem, one of the Millennium Prize problems, has been solved. The problem concerns technical properties of solutions to the Navier-Stokes equations [1], a set of equations that describe the dynamics of fluid flow. Popular accounts of the problem are often oversimplified and misleading. Some reports will speak of […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[260,9],"tags":[202,47],"class_list":["post-247864","post","type-post","status-publish","format-standard","hentry","category-ai","category-math","tag-artificial-intelligence","tag-differential-equations"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"Navier-Stokes in the news","description":"Navier-Stokes equations. What's the problem? What progress is being made? Is there Ai espionage going on?","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/08\/navier-stokes-in-the-news\/","robots":"max-image-preview:large","keywords":"artificial intelligence,differential equations","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"Navier-Stokes in the news","og:description":"Navier-Stokes equations. What's the problem? What progress is being made? Is there Ai espionage going on?","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/08\/navier-stokes-in-the-news\/","article:published_time":"2026-09-08T15:26:08+00:00","article:modified_time":"2026-09-08T17:48:11+00:00","twitter:card":"summary","twitter:title":"Navier-Stokes in the news","twitter:description":"Navier-Stokes equations. What's the problem? What progress is being made? Is there Ai espionage going on?","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247864","title":null,"description":"Navier-Stokes equations. What's the problem? What progress is being made? Is there Ai espionage going on?","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-08 14:17:10","updated":"2026-09-08 18:22:58","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"
\n\t\t\tHome<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tMath<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tNavier-Stokes in the news\n\t\t<\/span><\/div>","aioseo_breadcrumb_json":[{"label":"Home","link":"https:\/\/www.johndcook.com\/blog"},{"label":"Math","link":"https:\/\/www.johndcook.com\/blog\/category\/math\/"},{"label":"Navier-Stokes in the news","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/08\/navier-stokes-in-the-news\/"}],"_links":{"self":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247864","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/comments?post=247864"}],"version-history":[{"count":5,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247864\/revisions"}],"predecessor-version":[{"id":247867,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247864\/revisions\/247867"}],"wp:attachment":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/media?parent=247864"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/categories?post=247864"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/tags?post=247864"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}},{"id":247861,"date":"2026-09-07T13:35:45","date_gmt":"2026-09-07T18:35:45","guid":{"rendered":"https:\/\/www.johndcook.com\/blog\/?p=247861"},"modified":"2026-09-07T13:35:45","modified_gmt":"2026-09-07T18:35:45","slug":"ngram-error-rate","status":"publish","type":"post","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/07\/ngram-error-rate\/","title":{"rendered":"Ngram error rate"},"content":{"rendered":"The Online Etymological Dictionary gives the following etymology for\u00a0grok<\/em>:<\/span><\/p>\ngrok (v.)<\/p>\n
“understand empathically,” 1961, an arbitrary formation by U.S. science fiction writer Robert A. Heinlein (1907-1988) in his book “Stranger in a Strange Land.” In the book it is a transliteration of a Martian word and is said to mean etymologically “to drink.” It attained popular use in 1960s-70s counterculture but is perhaps obsolete now except in internet technology circles.<\/p><\/blockquote>\n
I don’t believe anything in the statement above is disputed. And yet Google’s Ngram Viewer tells a very different story.<\/p>\n
![](\"https:\/\/www.johndcook.com\/grok_ngram.png\")
<\/p>\n
The plot implies that use of the word\u00a0grok<\/em> had been increasing before Heinlein’s book came out and is now much more common than it was in the 1970s. Note that the plot ends before the Grok AI came out in late 2023.<\/p>\nApparently the Ngram data is unreliable, mainly for two reasons: OCR errors and inaccurate date attribution. Presumably the blip around 1900 was due to the former, OCR causing words like crok<\/em> or\u00a0grog<\/em> to be cataloged as\u00a0grok<\/em>. And presumably the rise in usage before 1961 was due to the latter, misattributing the date of sources published after 1961.<\/p>\nThe supposed rise in usage before 1961 is interesting. You’d expect some lag between the time a word circulates in conversation and when it appears in books, but apparently this lag can be smaller than the effect of date misattribution.<\/p>\n
Etymonline speculates that grok<\/em> is “perhaps obsolete now except in internet technology circles.” That matches my experience. Even in technological circles, the word was uncommon before Grok was released. Maybe it was more common in print than in conversation.<\/p>\nRelated posts<\/h2>\n
Previous posts with Ngram stats. The effects are so large that they’re probably directionally correct after adjusting for a substantial error rate.<\/p>\n
\n- Duodecimal vs. Hexadecimal<\/a><\/li>\n
- Orwellian vs. Huxleyian<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"
The Online Etymological Dictionary gives the following etymology for\u00a0grok: grok (v.) “understand empathically,” 1961, an arbitrary formation by U.S. science fiction writer Robert A. Heinlein (1907-1988) in his book “Stranger in a Strange Land.” In the book it is a transliteration of a Martian word and is said to mean etymologically “to drink.” It attained […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[1],"tags":[],"class_list":["post-247861","post","type-post","status-publish","format-standard","hentry","category-uncategorized"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"Ngram error rate","description":"An example illustrating the large amount of error in Ngram data.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/07\/ngram-error-rate\/","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"Ngram error rate","og:description":"An example illustrating the large amount of error in Ngram data.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/07\/ngram-error-rate\/","article:published_time":"2026-09-07T18:35:45+00:00","article:modified_time":"2026-09-07T18:35:45+00:00","twitter:card":"summary","twitter:title":"Ngram error rate","twitter:description":"An example illustrating the large amount of error in Ngram data.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247861","title":null,"description":"An example illustrating the large amount of error in Ngram data.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-07 17:52:02","updated":"2026-09-07 19:32:58","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"
\n\t\t\tHome<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tUncategorized<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tNgram error rate\n\t\t<\/span><\/div>","aioseo_breadcrumb_json":[{"label":"Home","link":"https:\/\/www.johndcook.com\/blog"},{"label":"Uncategorized","link":"https:\/\/www.johndcook.com\/blog\/category\/uncategorized\/"},{"label":"Ngram error rate","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/07\/ngram-error-rate\/"}],"_links":{"self":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247861","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/comments?post=247861"}],"version-history":[{"count":1,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247861\/revisions"}],"predecessor-version":[{"id":247862,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247861\/revisions\/247862"}],"wp:attachment":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/media?parent=247861"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/categories?post=247861"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/tags?post=247861"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}},{"id":247858,"date":"2026-09-05T12:04:13","date_gmt":"2026-09-05T17:04:13","guid":{"rendered":"https:\/\/www.johndcook.com\/blog\/?p=247858"},"modified":"2026-09-05T12:04:13","modified_gmt":"2026-09-05T17:04:13","slug":"proof-of-the-rank-trace-theorem","status":"publish","type":"post","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/05\/proof-of-the-rank-trace-theorem\/","title":{"rendered":"Proof of the rank-trace theorem"},"content":{"rendered":"The previous post<\/a> discussed the motivation for and application of the rank-trace theorem. This post will give a proof.<\/p>\nSuppose\u00a0A<\/em> is a real symmetric matrix. The rank-trace inequality says<\/p>\n![\"\\operatorname{rank}(A)\\ge\\frac{(\\operatorname{tr}](\"https:\/\/www.johndcook.com\/rank_trace1.svg\")
<\/p>\n
where tr is the trace operator, the sum of the elements along the diagonal of the matrix.<\/p>\n
Terse proof<\/h2>\n
Here’s the proof in a nutshell: diagonalize\u00a0A<\/em> and use the Cauchy-Schwarz inequality.<\/p>\nDetailed proof<\/h2>\n
Now let’s unpack that. Any real symmetric matrix A<\/em> is similar to a matrix D<\/em> with the eigenvalues of\u00a0A<\/em> along the diagonal.<\/p>\n![\"A](\"https:\/\/www.johndcook.com\/rank_trace2.svg\")
<\/p>\n
The trace of a matrix stays the same under a similarity transformation, i.e. multiplying by\u00a0P<\/em> on one side and its inverse on the other side. So without loss of generality we may as well assume\u00a0A<\/em> is diagonal.<\/p>\nThe rank of a matrix equals the number of non-zero eigenvalues, so a vector containing the non-zero eigenvalues of\u00a0A<\/em><\/p>\n![\"v](\"https:\/\/www.johndcook.com\/rank_trace3.svg\")
<\/p>\n
has length r<\/em> where r<\/em> is the rank of A<\/em>. Define w<\/em> to be the vector of dimension\u00a0r<\/em> consisting of all 1’s.<\/p>\n![\"w](\"https:\/\/www.johndcook.com\/rank_trace4.svg\")
<\/p>\n
Then by the Cauchy-Schwarz inequality we have<\/p>\n
![\"\\operatorname{tr}(A)^2](\"https:\/\/www.johndcook.com\/rank_trace6.svg\")
<\/p>\n
Cyclic trace property<\/h2>\n
Why should a matrix\u00a0A<\/em> and its diagonalization\u00a0D<\/em> have the same trace?<\/p>\nThe trace of a matrix product\u00a0AB<\/em> equals the trace of the product\u00a0BA<\/em>. To prove this, write out matrix products and the traces, then note that the two expressions are equal.<\/p>\n![\"](\"https:\/\/www.johndcook.com\/trace_commute.svg\")
<\/p>\n
Therefore<\/p>\n
![\"\\operatorname{tr}(A)](\"https:\/\/www.johndcook.com\/rank_trace7.svg\")
<\/p>\n
More generally, trace has the cyclic property<\/p>\n
![\"\\operatorname{tr}(ABC)](\"https:\/\/www.johndcook.com\/cycle_trace.svg\")
<\/p>\n
However, not all permutations preserve the trace. For example, let<\/p>\n
![\"A=\\begin{pmatrix}0&1\\\\0&0\\end{pmatrix},\\quad](\"https:\/\/www.johndcook.com\/rank_trace8.svg\")
<\/p>\n
Then<\/p>\n
![\"\\operatorname{tr}(ABC)](\"https:\/\/www.johndcook.com\/rank_trace11.svg\")
<\/p>\n
but<\/p>\n
![\"\\operatorname{tr}(ACB)](\"https:\/\/www.johndcook.com\/rank_trace10.svg\")
<\/p>\n","protected":false},"excerpt":{"rendered":"
The previous post discussed the motivation for and application of the rank-trace theorem. This post will give a proof. Suppose\u00a0A is a real symmetric matrix. The rank-trace inequality says where tr is the trace operator, the sum of the elements along the diagonal of the matrix. Terse proof Here’s the proof in a nutshell: diagonalize\u00a0A […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[9],"tags":[198],"class_list":["post-247858","post","type-post","status-publish","format-standard","hentry","category-math","tag-linear-algebra"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"Proof of the rank-trace theorem","description":"Proof of the rank-trace theorem. The cyclic property of the trace operator, and a counterexample to a plausible but false generalization.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/05\/proof-of-the-rank-trace-theorem\/","robots":"max-image-preview:large","keywords":"linear algebra","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"Proof of the rank-trace theorem","og:description":"Proof of the rank-trace theorem. The cyclic property of the trace operator, and a counterexample to a plausible but false generalization.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/05\/proof-of-the-rank-trace-theorem\/","article:published_time":"2026-09-05T17:04:13+00:00","article:modified_time":"2026-09-05T17:04:13+00:00","twitter:card":"summary","twitter:title":"Proof of the rank-trace theorem","twitter:description":"Proof of the rank-trace theorem. The cyclic property of the trace operator, and a counterexample to a plausible but false generalization.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247858","title":null,"description":"Proof of the rank-trace theorem. The cyclic property of the trace operator, and a counterexample to a plausible but false generalization.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-05 15:33:45","updated":"2026-09-05 17:38:00","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"
\n\t\t\tHome<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tMath<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tProof of the rank-trace theorem\n\t\t<\/span><\/div>","aioseo_breadcrumb_json":[{"label":"Home","link":"https:\/\/www.johndcook.com\/blog"},{"label":"Math","link":"https:\/\/www.johndcook.com\/blog\/category\/math\/"},{"label":"Proof of the rank-trace theorem","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/05\/proof-of-the-rank-trace-theorem\/"}],"_links":{"self":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247858","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/comments?post=247858"}],"version-history":[{"count":1,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247858\/revisions"}],"predecessor-version":[{"id":247859,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247858\/revisions\/247859"}],"wp:attachment":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/media?parent=247858"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/categories?post=247858"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/tags?post=247858"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}},{"id":247851,"date":"2026-09-04T09:16:16","date_gmt":"2026-09-04T14:16:16","guid":{"rendered":"https:\/\/www.johndcook.com\/blog\/?p=247851"},"modified":"2026-09-05T12:05:41","modified_gmt":"2026-09-05T17:05:41","slug":"stable-rank","status":"publish","type":"post","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/04\/stable-rank\/","title":{"rendered":"Computing a lower bound on matrix rank"},"content":{"rendered":"Suppose you want to know the rank of an n<\/em> \u00d7 n<\/em> matrix A<\/em>, the number of linearly independent rows of\u00a0A<\/em>, or equivalently the number of linearly independent columns. There are at least three difficulties.<\/p>\nDifficulties in computing rank<\/h2>\n
First of all, rank is not a continuous function of a matrix. Since rank is an integer, an arbitrarily small change in the matrix could cause a discrete change in the rank [1]. A small error in computing\u00a0A<\/em> could produce a matrix with a different rank.<\/p>\nSecond, finding the rank takes O<\/em>(n<\/em>\u00b3) operations, which may or may not be an issue depending on context.<\/p>\nThird, you may not have the matrix\u00a0A<\/em> in an explicit form. Maybe you’re able to compute products\u00a0Av<\/em> for vectors\u00a0v<\/em> but it’s not practical to form the entire matrix\u00a0A<\/em>.<\/p>\nRank-trace inequality<\/h2>\n
If you don’t need to know the rank of\u00a0A<\/em> per se, but only need to know whether it is above a certain size, a lower bound on the rank may enough.<\/p>\nSuppose\u00a0A<\/em> is a Hermitian matrix. If\u00a0A<\/em> is real, this means\u00a0A<\/em> is symmetric. If\u00a0A<\/em> is complex, this means\u00a0A<\/em> equals its conjugate transpose. Then the rank-trace inequality says<\/p>\n
\nThe quantity on the right hand side is known as the stable rank<\/strong> of\u00a0A<\/em>. It’s not a rank in any algebraic sense, but it gives a lower bound on rank. And it solves the three problems listed above. See the next post<\/a> for a proof of the rank-trace theorem.<\/p>\nStability<\/h3>\n
First of all, trace\u00a0is<\/em> a continuous function of a matrix, and so stable rank is also a continuous function of a matrix, provided the denominator isn’t zero. A small change to a matrix only makes a small change to its stable rank. That’s why stable rank is called stable.<\/p>\nEfficiency<\/h3>\n
Second, although computing rank takes O<\/em>(n<\/em>\u00b3) operations, computing stable rank\u00a0takes only O<\/em>(n<\/em>\u00b2) operations, though this isn’t immediately obvious.<\/p>\nThe trace of A<\/em> takes n<\/em> operations: simply sum the elements on the diagonal of A<\/em>. But how do you take the trace of A<\/em>\u00b2? Squaring A<\/em> takes n<\/em>\u00b3 operations, and so if you had to square A<\/em> to find the trace of A<\/em>\u00b2 the rank-trace inequality would have no efficiency advantage over finding the rank of A<\/em>. But you can compute the trace of A<\/em>\u00b2 via<\/p>\n![\"\\operatorname{tr}(A^2)](\"https:\/\/www.johndcook.com\/trace_A2.svg\")
<\/p>\n
Formation<\/h3>\n
Now suppose you don’t have the matrix A<\/em> per se but you do have a way of probing A<\/em>, computing the product of vectors with A<\/em>. Maybe A<\/em> is too large to fit into memory, or explicitly computing the elements of A<\/em> would take too long.<\/p>\nThere are Monte Carlo algorithms for estimating the traces of A<\/em> and A<\/em>\u00b2 that could be used together to estimate the stable rank of A<\/em>.<\/p>\nDemonstration<\/h2>\n
The following Python code illustrates the discussion above.<\/p>\n
import numpy as np\r\n\r\nnp.random.seed(20260904)\r\nn = 5\r\nB = np.random.randn(n, n)\r\nA = B.T @ B + 1e-8 * np.eye(n) # Gram matrix plus a tiny shift => SPD\r\n\r\nrank_A = np.linalg.matrix_rank(A)\r\ntr_A = np.trace(A)\r\ntr_A2 = np.trace(A @ A) # matrix product \r\nsum_sq = np.sum(A * A) # element-by-element product\r\nstable_rank = (tr_A ** 2) \/ tr_A2\r\n\r\nprint(f\"A =\\n{A}\\n\")\r\nprint(f\"rank(A) = {rank_A}\")\r\nprint(f\"tr(A) = {tr_A:.12f}\")\r\nprint(f\"tr(A^2) direct = {tr_A2:.12f}\")\r\nprint(f\"tr(A^2) indirect = {sum_sq:.12f}\")\r\nprint(f\"stable rank = {stable_rank:.12f}\")\r\n<\/pre>\nThe code above produces the output below.<\/p>\n
A =\r\n[[ 1.09945682 0.4899665 0.98901845 0.66983113 -1.35006341]\r\n [ 0.4899665 0.98531254 0.35067791 0.89757603 -0.72037507]\r\n [ 0.98901845 0.35067791 4.31233926 0.94556225 -0.54819048]\r\n [ 0.66983113 0.89757603 0.94556225 1.3494295 -1.33840786]\r\n [-1.35006341 -0.72037507 -0.54819048 -1.33840786 3.54858332]]\r\n\r\nrank(A) = 5\r\ntr(A) = 11.295121449420\r\ntr(A^2) direct = 51.035447533673\r\ntr(A^2) indirect = 51.035447533673\r\nstable rank = 2.499826585688\r\n<\/pre>\n[1] Topological argument: A map from a connected space (such as \u211dn<\/em>\u00d7n<\/em><\/sup>) onto a discrete space (such as \u2124) cannot be continuous, otherwise the inverse images of the points in the range would partition the connected space into disjoint open sets, violating the definition of a connected space.<\/p>\n","protected":false},"excerpt":{"rendered":"Suppose you want to know the rank of an n \u00d7 n matrix A, the number of linearly independent rows of\u00a0A, or equivalently the number of linearly independent columns. There are at least three difficulties. Difficulties in computing rank First of all, rank is not a continuous function of a matrix. Since rank is an […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[5,9],"tags":[198],"class_list":["post-247851","post","type-post","status-publish","format-standard","hentry","category-computing","category-math","tag-linear-algebra"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"Computing a lower bound on matrix rank","description":"Why computing the rank of a matrix can be difficult and how the rank-trace inequality lower bound solves the difficulties if a lower bound is adequate.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/04\/stable-rank\/","robots":"max-image-preview:large","keywords":"linear algebra","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"Computing a lower bound on matrix rank","og:description":"Why computing the rank of a matrix can be difficult and how the rank-trace inequality lower bound solves the difficulties if a lower bound is adequate.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/04\/stable-rank\/","article:published_time":"2026-09-04T14:16:16+00:00","article:modified_time":"2026-09-05T17:05:41+00:00","twitter:card":"summary","twitter:title":"Computing a lower bound on matrix rank","twitter:description":"Why computing the rank of a matrix can be difficult and how the rank-trace inequality lower bound solves the difficulties if a lower bound is adequate.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247851","title":null,"description":"Why computing the rank of a matrix can be difficult and how the rank-trace inequality lower bound solves the difficulties if a lower bound is adequate.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-04 13:08:46","updated":"2026-09-05 17:38:00","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"
\n\t\t\tHome<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tComputing<\/a>\n\t\t<\/span>»<\/span>\n\t\t\tComputing a lower bound on matrix rank\n\t\t<\/span><\/div>","aioseo_breadcrumb_json":[{"label":"Home","link":"https:\/\/www.johndcook.com\/blog"},{"label":"Computing","link":"https:\/\/www.johndcook.com\/blog\/category\/computing\/"},{"label":"Computing a lower bound on matrix rank","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/04\/stable-rank\/"}],"_links":{"self":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247851","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/comments?post=247851"}],"version-history":[{"count":6,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247851\/revisions"}],"predecessor-version":[{"id":247860,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/posts\/247851\/revisions\/247860"}],"wp:attachment":[{"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/media?parent=247851"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/categories?post=247851"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.johndcook.com\/blog\/wp-json\/wp\/v2\/tags?post=247851"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}},{"id":247847,"date":"2026-09-03T18:34:41","date_gmt":"2026-09-03T23:34:41","guid":{"rendered":"https:\/\/www.johndcook.com\/blog\/?p=247847"},"modified":"2026-09-04T06:01:12","modified_gmt":"2026-09-04T11:01:12","slug":"hugging-face-easter-egg","status":"publish","type":"post","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/03\/hugging-face-easter-egg\/","title":{"rendered":"Hugging Face Easter Egg"},"content":{"rendered":"NVIDIA has offered to buy Hugging Face for $12,930,300,000.<\/p>\n
129303 is the Unicode code point for the Hugging Face emoj (U+1F917), which you can verify with the following Python code.<\/p>\n
\r\n>>> import unicodedata\r\n>>> 129303 == 0x1F917\r\nTrue\r\n>>> unicodedata.name(chr(0x1F917))\r\n'HUGGING FACE'\r\n<\/pre>\n![\"Hugging](\"https:\/\/www.johndcook.com\/huggingface.png\")
<\/p>\n
Related posts<\/h2>\n\n- Prevent characters from displaying as emoji<\/a><\/li>\n
- Unicode, Tolkien, and Privacy<\/a><\/li>\n
- Unicode surrogates<\/a><\/li>\n
- Making flags in Unicode<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"
NVIDIA has offered to buy Hugging Face for $12,930,300,000. 129303 is the Unicode code point for the Hugging Face emoj (U+1F917), which you can verify with the following Python code. >>> import unicodedata >>> 129303 == 0x1F917 True >>> unicodedata.name(chr(0x1F917)) ‘HUGGING FACE’ Related posts Prevent characters from displaying as emoji Unicode, Tolkien, and Privacy Unicode […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[1],"tags":[135],"class_list":["post-247847","post","type-post","status-publish","format-standard","hentry","category-uncategorized","tag-unicode"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"Hugging Face Easter Egg","description":"Unicode Easter Egg in NVIDIA's offer to buy Hugging Face","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/03\/hugging-face-easter-egg\/","robots":"max-image-preview:large","keywords":"unicode","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"Hugging Face Easter Egg","og:description":"Unicode Easter Egg in NVIDIA's offer to buy Hugging Face","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/03\/hugging-face-easter-egg\/","article:published_time":"2026-09-03T23:34:41+00:00","article:modified_time":"2026-09-04T11:01:12+00:00","twitter:card":"summary","twitter:title":"Hugging Face Easter Egg","twitter:description":"Unicode Easter Egg in NVIDIA's offer to buy Hugging Face","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247847","title":null,"description":"Unicode Easter Egg in NVIDIA's offer to buy Hugging Face","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-03 23:15:55","updated":"2026-09-04 11:34:04","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"
[1] John A. Koch was a programmer who worked on the four color proof with Haken and Appel. I don’t know how much credit he deserves, but I suspect it may be more than he was given.<\/p>\n","protected":false},"excerpt":{"rendered":"
The idea of using computers to assist with proofs is not new. The first major computer-assisted proof was published in 1976, the proof of the four color theorem by Kenneth Appel and Wolfgang Haken. The authors reduced the proof of the four color theorem to verifying calculations on 1,834 configurations, each checked by a computer […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[5],"tags":[],"class_list":["post-247877","post","type-post","status-publish","format-standard","hentry","category-computing"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"A 50-year-old computer-assisted proof","description":"Computer-assisted proofs are older than you may imagine. The first major theorem proved with the assistance of a computer was over 50 years ago.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/four-colors\/","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"A 50-year-old computer-assisted proof","og:description":"Computer-assisted proofs are older than you may imagine. The first major theorem proved with the assistance of a computer was over 50 years ago.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/four-colors\/","article:published_time":"2026-09-09T14:59:48+00:00","article:modified_time":"2026-09-09T14:59:48+00:00","twitter:card":"summary","twitter:title":"A 50-year-old computer-assisted proof","twitter:description":"Computer-assisted proofs are older than you may imagine. The first major theorem proved with the assistance of a computer was over 50 years ago.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247877","title":null,"description":"Computer-assisted proofs are older than you may imagine. The first major theorem proved with the assistance of a computer was over 50 years ago.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-09 14:24:10","updated":"2026-09-09 14:59:48","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"
A rising tide may lift all boats, but the AI tide lifts some boats much more than others.<\/p>\n
By all accounts, the best programmers have had the biggest productivity boost from AI. And top tier mathematicians are using AI to settle long-standing mathematical conjectures. AI is a powerful tool, but tools don’t come to life and make things on their own.<\/p>\n
I routinely have naive amateurs send me proofs of open conjectures, and naturally more recent such proofs involve AI. I’ll get an email saying something like “I’ve solved the Collatz conjecture using ChatGPT, but I’m not a mathematician so I need some help verifying the proof.” And of course the supposed proof is rubbish.<\/p>\n
The recent Navier-Stokes proof is impressive, but AI didn’t initiate the proof any more than LaTeX did. Nor did a child steer AI into proving the conjecture. Professional mathematicians were able to use AI to pursue their ideas at superhuman speed. But someone without an understanding of the Navier-Stokes problem, and familiarity with recent ideas for approaching the problem, could not have directed AI to produce a proof. <\/p>\n
Computer scientists have been saying “garbage in, garbage out” from the beginning. A variation on this aphorism for the age of AI would be “mediocrity in, mediocrity out.” <\/p>\n","protected":false},"excerpt":{"rendered":"
A rising tide may lift all boats, but the AI tide lifts some boats much more than others. By all accounts, the best programmers have had the biggest productivity boost from AI. And top tier mathematicians are using AI to settle long-standing mathematical conjectures. AI is a powerful tool, but tools don’t come to life […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[260],"tags":[],"class_list":["post-247875","post","type-post","status-publish","format-standard","hentry","category-ai"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"AI is an intelligence multiplier","description":"The most productive, most creative, and most intelligent people will benefit the most from AI.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/ai-multiplier\/","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"AI is an intelligence multiplier","og:description":"The most productive, most creative, and most intelligent people will benefit the most from AI.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/ai-multiplier\/","article:published_time":"2026-09-09T14:17:20+00:00","article:modified_time":"2026-09-09T14:17:20+00:00","twitter:card":"summary","twitter:title":"AI is an intelligence multiplier","twitter:description":"The most productive, most creative, and most intelligent people will benefit the most from AI.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247875","title":null,"description":"The most productive, most creative, and most intelligent people will benefit the most from AI.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-09 13:47:02","updated":"2026-09-09 14:17:21","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"
Yesterday OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics. The announcement has created a lot of buzz, as one would expect. But there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as their conventional human-readable proof.<\/p>\n
Quite a few other mathematical conjectures have been settled recently using AI, and these have also been accompanied with formal proofs, using Lean 4 in particular.<\/p>\n
Until very recently, generating machine-verifiable formal proofs has been excruciatingly tedious<\/strong>. In 2005, Henk Barendregt and Freek Wiedijk wrote<\/a><\/p>\n To give an indication of how much work is needed for formalisation, we estimate that it takes approximately one work-week (five work-days of eight work-hours) to formalise one page from an undergraduate mathematics textbook.<\/p><\/blockquote>\n That was the rule of thumb: forty hours per page<\/strong>. And this in the context of undergraduate textbooks. Research publications are much denser than textbooks. Furthermore, page 100 of a textbook probably depends mostly on material on pages 1 through 99. A sentence in a research article could cite anything that has been published before.<\/p>\n Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook. Then formalizing the 166-page paper from OpenAI would take 132,800 person-hours. It took OpenAI 17 hours to verify their proof in Lean. I hesitate to use the word “revolutionary,” but lowering the cost of anything by four orders of magnitude<\/strong> is revolutionary.<\/p>\n I’ve used AI to generate formal proofs to check my work just for a little blog post. I wouldn’t dream of doing that if I had to pay someone a week’s salary to check my work.<\/p>\n Formal verification doesn’t just apply to mathematics. You could, for example, formally verify that a set of security policies are consistent and that, given certain assumptions, they accomplish their purpose. You could formally verify that a smart contract imposes a certain maximum liability. You could verify the correctness of mission-critical algorithms. These problems are easier than formalizing mathematics research, and it is easier to quantify the return on investment.<\/p>\n Yesterday OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics. The announcement has created a lot of buzz, as one would expect. But there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[1],"tags":[324],"class_list":["post-247870","post","type-post","status-publish","format-standard","hentry","category-uncategorized","tag-formal-methods"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"The part of Navier-Stokes no one is talking about","description":"When OpenAI released their proof that solutions to the Navier-Stokes equations can blow up in finite time, they also released a formal proof in Lean 4.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/formal-method-revolution\/","robots":"max-image-preview:large","keywords":"formal methods","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"The part of Navier-Stokes no one is talking about","og:description":"When OpenAI released their proof that solutions to the Navier-Stokes equations can blow up in finite time, they also released a formal proof in Lean 4.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/formal-method-revolution\/","article:published_time":"2026-09-09T12:43:36+00:00","article:modified_time":"2026-09-09T12:43:36+00:00","twitter:card":"summary","twitter:title":"The part of Navier-Stokes no one is talking about","twitter:description":"When OpenAI released their proof that solutions to the Navier-Stokes equations can blow up in finite time, they also released a formal proof in Lean 4.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247870","title":null,"description":"When OpenAI released their proof that solutions to the Navier-Stokes equations can blow up in finite time, they also released a formal proof in Lean 4.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-09 11:31:29","updated":"2026-09-09 13:05:58","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":" There are rumors that a long-standing math problem, one of the Millennium Prize problems, has been solved.<\/p>\n The problem concerns technical properties of solutions to the Navier-Stokes equations<\/strong> [1], a set of equations that describe the dynamics of fluid flow. Popular accounts of the problem are often oversimplified and misleading.<\/p>\n Some reports will speak of the problem as “solving the Navier-Stokes equations.” The task is not to write down a closed-form solution, which can’t be done, or solve the equations numerically, which has been done for decades. The problem is to prove theoretical properties of solutions which are of little interest in practice.<\/p>\n There has been progress toward settling the Navier-Stokes problem. Terence Tao wrote a post on this yesterday<\/a>.<\/p>\n What’s also\u00a0 interesting is the intrigue around the possible solution. A post<\/a> this morning says<\/p>\n If I am reading this correctly, Tristan Buckmaster is alleging OAI has a resolution of Navier-Stokes \u2026 which maybe used info from Buckmaster and Levent Alp\u00f6ge\u2019s private Codex sessions.<\/p><\/blockquote>\n Buckmaster asked OpenAI whether they used his private sessions and they have not responded. Update<\/strong>: Statement<\/a> from OpenAI.<\/p>\n This topic connects parts of my career spanning decades. My graduate work was in PDEs and I had some interest in the Navier-Stokes equations. Here are some notes<\/a> I wrote back in the day.<\/p>\n Now I work more with privacy than with PDEs. The question of whether OpenAI uses private data, contradicting their stated policy, is more relevant to my current work than whether the Navier-Stokes equations have global regular solutions.<\/p>\n [1] I never know whether to say equation or equations. You’ll hear both. You could think of Navier-Stokes as one vector-valued PDE or three scalar-valued equations.<\/p>\n","protected":false},"excerpt":{"rendered":" There are rumors that a long-standing math problem, one of the Millennium Prize problems, has been solved. The problem concerns technical properties of solutions to the Navier-Stokes equations [1], a set of equations that describe the dynamics of fluid flow. Popular accounts of the problem are often oversimplified and misleading. Some reports will speak of […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[260,9],"tags":[202,47],"class_list":["post-247864","post","type-post","status-publish","format-standard","hentry","category-ai","category-math","tag-artificial-intelligence","tag-differential-equations"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"Navier-Stokes in the news","description":"Navier-Stokes equations. What's the problem? What progress is being made? Is there Ai espionage going on?","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/08\/navier-stokes-in-the-news\/","robots":"max-image-preview:large","keywords":"artificial intelligence,differential equations","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"Navier-Stokes in the news","og:description":"Navier-Stokes equations. What's the problem? What progress is being made? Is there Ai espionage going on?","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/08\/navier-stokes-in-the-news\/","article:published_time":"2026-09-08T15:26:08+00:00","article:modified_time":"2026-09-08T17:48:11+00:00","twitter:card":"summary","twitter:title":"Navier-Stokes in the news","twitter:description":"Navier-Stokes equations. What's the problem? What progress is being made? Is there Ai espionage going on?","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247864","title":null,"description":"Navier-Stokes equations. What's the problem? What progress is being made? Is there Ai espionage going on?","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-08 14:17:10","updated":"2026-09-08 18:22:58","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":" The Online Etymological Dictionary gives the following etymology for\u00a0grok<\/em>:<\/span><\/p>\n grok (v.)<\/p>\n “understand empathically,” 1961, an arbitrary formation by U.S. science fiction writer Robert A. Heinlein (1907-1988) in his book “Stranger in a Strange Land.” In the book it is a transliteration of a Martian word and is said to mean etymologically “to drink.” It attained popular use in 1960s-70s counterculture but is perhaps obsolete now except in internet technology circles.<\/p><\/blockquote>\n I don’t believe anything in the statement above is disputed. And yet Google’s Ngram Viewer tells a very different story.<\/p>\n The plot implies that use of the word\u00a0grok<\/em> had been increasing before Heinlein’s book came out and is now much more common than it was in the 1970s. Note that the plot ends before the Grok AI came out in late 2023.<\/p>\n Apparently the Ngram data is unreliable, mainly for two reasons: OCR errors and inaccurate date attribution. Presumably the blip around 1900 was due to the former, OCR causing words like crok<\/em> or\u00a0grog<\/em> to be cataloged as\u00a0grok<\/em>. And presumably the rise in usage before 1961 was due to the latter, misattributing the date of sources published after 1961.<\/p>\n The supposed rise in usage before 1961 is interesting. You’d expect some lag between the time a word circulates in conversation and when it appears in books, but apparently this lag can be smaller than the effect of date misattribution.<\/p>\n Etymonline speculates that grok<\/em> is “perhaps obsolete now except in internet technology circles.” That matches my experience. Even in technological circles, the word was uncommon before Grok was released. Maybe it was more common in print than in conversation.<\/p>\n Previous posts with Ngram stats. The effects are so large that they’re probably directionally correct after adjusting for a substantial error rate.<\/p>\n The Online Etymological Dictionary gives the following etymology for\u00a0grok: grok (v.) “understand empathically,” 1961, an arbitrary formation by U.S. science fiction writer Robert A. Heinlein (1907-1988) in his book “Stranger in a Strange Land.” In the book it is a transliteration of a Martian word and is said to mean etymologically “to drink.” It attained […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[1],"tags":[],"class_list":["post-247861","post","type-post","status-publish","format-standard","hentry","category-uncategorized"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"Ngram error rate","description":"An example illustrating the large amount of error in Ngram data.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/07\/ngram-error-rate\/","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"Ngram error rate","og:description":"An example illustrating the large amount of error in Ngram data.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/07\/ngram-error-rate\/","article:published_time":"2026-09-07T18:35:45+00:00","article:modified_time":"2026-09-07T18:35:45+00:00","twitter:card":"summary","twitter:title":"Ngram error rate","twitter:description":"An example illustrating the large amount of error in Ngram data.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247861","title":null,"description":"An example illustrating the large amount of error in Ngram data.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-07 17:52:02","updated":"2026-09-07 19:32:58","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":" The previous post<\/a> discussed the motivation for and application of the rank-trace theorem. This post will give a proof.<\/p>\n Suppose\u00a0A<\/em> is a real symmetric matrix. The rank-trace inequality says<\/p>\n where tr is the trace operator, the sum of the elements along the diagonal of the matrix.<\/p>\n Here’s the proof in a nutshell: diagonalize\u00a0A<\/em> and use the Cauchy-Schwarz inequality.<\/p>\n Now let’s unpack that. Any real symmetric matrix A<\/em> is similar to a matrix D<\/em> with the eigenvalues of\u00a0A<\/em> along the diagonal.<\/p>\n The trace of a matrix stays the same under a similarity transformation, i.e. multiplying by\u00a0P<\/em> on one side and its inverse on the other side. So without loss of generality we may as well assume\u00a0A<\/em> is diagonal.<\/p>\n The rank of a matrix equals the number of non-zero eigenvalues, so a vector containing the non-zero eigenvalues of\u00a0A<\/em><\/p>\n has length r<\/em> where r<\/em> is the rank of A<\/em>. Define w<\/em> to be the vector of dimension\u00a0r<\/em> consisting of all 1’s.<\/p>\n Then by the Cauchy-Schwarz inequality we have<\/p>\n Why should a matrix\u00a0A<\/em> and its diagonalization\u00a0D<\/em> have the same trace?<\/p>\n The trace of a matrix product\u00a0AB<\/em> equals the trace of the product\u00a0BA<\/em>. To prove this, write out matrix products and the traces, then note that the two expressions are equal.<\/p>\n Therefore<\/p>\n More generally, trace has the cyclic property<\/p>\n However, not all permutations preserve the trace. For example, let<\/p>\n Then<\/p>\n but<\/p>\n The previous post discussed the motivation for and application of the rank-trace theorem. This post will give a proof. Suppose\u00a0A is a real symmetric matrix. The rank-trace inequality says where tr is the trace operator, the sum of the elements along the diagonal of the matrix. Terse proof Here’s the proof in a nutshell: diagonalize\u00a0A […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[9],"tags":[198],"class_list":["post-247858","post","type-post","status-publish","format-standard","hentry","category-math","tag-linear-algebra"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"Proof of the rank-trace theorem","description":"Proof of the rank-trace theorem. The cyclic property of the trace operator, and a counterexample to a plausible but false generalization.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/05\/proof-of-the-rank-trace-theorem\/","robots":"max-image-preview:large","keywords":"linear algebra","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"Proof of the rank-trace theorem","og:description":"Proof of the rank-trace theorem. The cyclic property of the trace operator, and a counterexample to a plausible but false generalization.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/05\/proof-of-the-rank-trace-theorem\/","article:published_time":"2026-09-05T17:04:13+00:00","article:modified_time":"2026-09-05T17:04:13+00:00","twitter:card":"summary","twitter:title":"Proof of the rank-trace theorem","twitter:description":"Proof of the rank-trace theorem. The cyclic property of the trace operator, and a counterexample to a plausible but false generalization.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247858","title":null,"description":"Proof of the rank-trace theorem. The cyclic property of the trace operator, and a counterexample to a plausible but false generalization.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-05 15:33:45","updated":"2026-09-05 17:38:00","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":" Suppose you want to know the rank of an n<\/em> \u00d7 n<\/em> matrix A<\/em>, the number of linearly independent rows of\u00a0A<\/em>, or equivalently the number of linearly independent columns. There are at least three difficulties.<\/p>\n First of all, rank is not a continuous function of a matrix. Since rank is an integer, an arbitrarily small change in the matrix could cause a discrete change in the rank [1]. A small error in computing\u00a0A<\/em> could produce a matrix with a different rank.<\/p>\n Second, finding the rank takes O<\/em>(n<\/em>\u00b3) operations, which may or may not be an issue depending on context.<\/p>\n Third, you may not have the matrix\u00a0A<\/em> in an explicit form. Maybe you’re able to compute products\u00a0Av<\/em> for vectors\u00a0v<\/em> but it’s not practical to form the entire matrix\u00a0A<\/em>.<\/p>\n If you don’t need to know the rank of\u00a0A<\/em> per se, but only need to know whether it is above a certain size, a lower bound on the rank may enough.<\/p>\n Suppose\u00a0A<\/em> is a Hermitian matrix. If\u00a0A<\/em> is real, this means\u00a0A<\/em> is symmetric. If\u00a0A<\/em> is complex, this means\u00a0A<\/em> equals its conjugate transpose. Then the rank-trace inequality says<\/p>\n First of all, trace\u00a0is<\/em> a continuous function of a matrix, and so stable rank is also a continuous function of a matrix, provided the denominator isn’t zero. A small change to a matrix only makes a small change to its stable rank. That’s why stable rank is called stable.<\/p>\n Second, although computing rank takes O<\/em>(n<\/em>\u00b3) operations, computing stable rank\u00a0takes only O<\/em>(n<\/em>\u00b2) operations, though this isn’t immediately obvious.<\/p>\n The trace of A<\/em> takes n<\/em> operations: simply sum the elements on the diagonal of A<\/em>. But how do you take the trace of A<\/em>\u00b2? Squaring A<\/em> takes n<\/em>\u00b3 operations, and so if you had to square A<\/em> to find the trace of A<\/em>\u00b2 the rank-trace inequality would have no efficiency advantage over finding the rank of A<\/em>. But you can compute the trace of A<\/em>\u00b2 via<\/p>\n Now suppose you don’t have the matrix A<\/em> per se but you do have a way of probing A<\/em>, computing the product of vectors with A<\/em>. Maybe A<\/em> is too large to fit into memory, or explicitly computing the elements of A<\/em> would take too long.<\/p>\n There are Monte Carlo algorithms for estimating the traces of A<\/em> and A<\/em>\u00b2 that could be used together to estimate the stable rank of A<\/em>.<\/p>\n The following Python code illustrates the discussion above.<\/p>\n The code above produces the output below.<\/p>\n [1] Topological argument: A map from a connected space (such as \u211dn<\/em>\u00d7n<\/em><\/sup>) onto a discrete space (such as \u2124) cannot be continuous, otherwise the inverse images of the points in the range would partition the connected space into disjoint open sets, violating the definition of a connected space.<\/p>\n","protected":false},"excerpt":{"rendered":" Suppose you want to know the rank of an n \u00d7 n matrix A, the number of linearly independent rows of\u00a0A, or equivalently the number of linearly independent columns. There are at least three difficulties. Difficulties in computing rank First of all, rank is not a continuous function of a matrix. Since rank is an […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[5,9],"tags":[198],"class_list":["post-247851","post","type-post","status-publish","format-standard","hentry","category-computing","category-math","tag-linear-algebra"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"Computing a lower bound on matrix rank","description":"Why computing the rank of a matrix can be difficult and how the rank-trace inequality lower bound solves the difficulties if a lower bound is adequate.","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/04\/stable-rank\/","robots":"max-image-preview:large","keywords":"linear algebra","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"Computing a lower bound on matrix rank","og:description":"Why computing the rank of a matrix can be difficult and how the rank-trace inequality lower bound solves the difficulties if a lower bound is adequate.","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/04\/stable-rank\/","article:published_time":"2026-09-04T14:16:16+00:00","article:modified_time":"2026-09-05T17:05:41+00:00","twitter:card":"summary","twitter:title":"Computing a lower bound on matrix rank","twitter:description":"Why computing the rank of a matrix can be difficult and how the rank-trace inequality lower bound solves the difficulties if a lower bound is adequate.","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247851","title":null,"description":"Why computing the rank of a matrix can be difficult and how the rank-trace inequality lower bound solves the difficulties if a lower bound is adequate.","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-04 13:08:46","updated":"2026-09-05 17:38:00","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":" NVIDIA has offered to buy Hugging Face for $12,930,300,000.<\/p>\n 129303 is the Unicode code point for the Hugging Face emoj (U+1F917), which you can verify with the following Python code.<\/p>\n NVIDIA has offered to buy Hugging Face for $12,930,300,000. 129303 is the Unicode code point for the Hugging Face emoj (U+1F917), which you can verify with the following Python code. >>> import unicodedata >>> 129303 == 0x1F917 True >>> unicodedata.name(chr(0x1F917)) ‘HUGGING FACE’ Related posts Prevent characters from displaying as emoji Unicode, Tolkien, and Privacy Unicode […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[1],"tags":[135],"class_list":["post-247847","post","type-post","status-publish","format-standard","hentry","category-uncategorized","tag-unicode"],"acf":[],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"Hugging Face Easter Egg","description":"Unicode Easter Egg in NVIDIA's offer to buy Hugging Face","canonical_url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/03\/hugging-face-easter-egg\/","robots":"max-image-preview:large","keywords":"unicode","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"en_US","og:site_name":"John D. Cook | Applied Mathematics Consulting","og:type":"article","og:title":"Hugging Face Easter Egg","og:description":"Unicode Easter Egg in NVIDIA's offer to buy Hugging Face","og:url":"https:\/\/www.johndcook.com\/blog\/2026\/09\/03\/hugging-face-easter-egg\/","article:published_time":"2026-09-03T23:34:41+00:00","article:modified_time":"2026-09-04T11:01:12+00:00","twitter:card":"summary","twitter:title":"Hugging Face Easter Egg","twitter:description":"Unicode Easter Egg in NVIDIA's offer to buy Hugging Face","twitter:image":"https:\/\/www.johndcook.com\/blog\/wp-content\/uploads\/2022\/05\/twittercard.png"},"aioseo_meta_data":{"post_id":"247847","title":null,"description":"Unicode Easter Egg in NVIDIA's offer to buy Hugging Face","keywords":null,"keyphrases":{"focus":{"keyphrase":"","score":0,"analysis":{"keyphraseInTitle":{"score":0,"maxScore":9,"error":1}}},"additional":[]},"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":"","og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"Article","isEnabled":true},"graphs":[]},"schema_type":"default","schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":"-1","robots_max_videopreview":"-1","robots_max_imagepreview":"large","priority":null,"frequency":"default","location":null,"local_seo":null,"breadcrumb_settings":null,"limit_modified_date":false,"created":"2026-09-03 23:15:55","updated":"2026-09-04 11:34:04","ai":{"faqs":[],"keyPoints":[],"schemas":[],"titles":[],"descriptions":[],"socialPosts":{"email":{"subject":"","preview":"","content":""},"linkedin":[],"twitter":[],"facebook":[],"instagram":[]}},"seo_analyzer_scan_date":null,"focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"aioseo_breadcrumb":"Related posts<\/h2>\n
\n
Personal note<\/h2>\n
Related posts<\/h2>\n
\n
<\/p>\nRelated posts<\/h2>\n
\n
<\/p>\nTerse proof<\/h2>\n
Detailed proof<\/h2>\n
<\/p>\n<\/p>\n<\/p>\n<\/p>\nCyclic trace property<\/h2>\n
<\/p>\n<\/p>\n<\/p>\n<\/p>\n<\/p>\n<\/p>\n","protected":false},"excerpt":{"rendered":"Difficulties in computing rank<\/h2>\n
Rank-trace inequality<\/h2>\n
\nThe quantity on the right hand side is known as the stable rank<\/strong> of\u00a0A<\/em>. It’s not a rank in any algebraic sense, but it gives a lower bound on rank. And it solves the three problems listed above. See the next post<\/a> for a proof of the rank-trace theorem.<\/p>\nStability<\/h3>\n
Efficiency<\/h3>\n
<\/p>\nFormation<\/h3>\n
Demonstration<\/h2>\n
import numpy as np\r\n\r\nnp.random.seed(20260904)\r\nn = 5\r\nB = np.random.randn(n, n)\r\nA = B.T @ B + 1e-8 * np.eye(n) # Gram matrix plus a tiny shift => SPD\r\n\r\nrank_A = np.linalg.matrix_rank(A)\r\ntr_A = np.trace(A)\r\ntr_A2 = np.trace(A @ A) # matrix product \r\nsum_sq = np.sum(A * A) # element-by-element product\r\nstable_rank = (tr_A ** 2) \/ tr_A2\r\n\r\nprint(f\"A =\\n{A}\\n\")\r\nprint(f\"rank(A) = {rank_A}\")\r\nprint(f\"tr(A) = {tr_A:.12f}\")\r\nprint(f\"tr(A^2) direct = {tr_A2:.12f}\")\r\nprint(f\"tr(A^2) indirect = {sum_sq:.12f}\")\r\nprint(f\"stable rank = {stable_rank:.12f}\")\r\n<\/pre>\nA =\r\n[[ 1.09945682 0.4899665 0.98901845 0.66983113 -1.35006341]\r\n [ 0.4899665 0.98531254 0.35067791 0.89757603 -0.72037507]\r\n [ 0.98901845 0.35067791 4.31233926 0.94556225 -0.54819048]\r\n [ 0.66983113 0.89757603 0.94556225 1.3494295 -1.33840786]\r\n [-1.35006341 -0.72037507 -0.54819048 -1.33840786 3.54858332]]\r\n\r\nrank(A) = 5\r\ntr(A) = 11.295121449420\r\ntr(A^2) direct = 51.035447533673\r\ntr(A^2) indirect = 51.035447533673\r\nstable rank = 2.499826585688\r\n<\/pre>\n
\r\n>>> import unicodedata\r\n>>> 129303 == 0x1F917\r\nTrue\r\n>>> unicodedata.name(chr(0x1F917))\r\n'HUGGING FACE'\r\n<\/pre>\n
<\/p>\nRelated posts<\/h2>\n
\n