Ciro Santilli @cirosantilli 40

When Ciro Santilli first learnt the old Zermelo-Fraenkel set theory and the idea of formal proofs, his teenager mind was completely blown.

Finally, there it was: a proper and precise definition of mathematics, including a definition of integers, reals and limits!

Theorems are strings, proofs are string manipulations, and axioms are the initial strings that you can use.

Once proved, press a button on your computer, and the proof is automatically verified. No messy complicated "group of savants" reading it for 4 years and looking for flaws!

There are a few proof assistant systems with several theorems in their Git tracked standard library. The hottest ones circa 2020 are:

And here are some more interesting links:

However, as expressed by the QED manifesto, is unbelievable that there isn't one awesome and dominating website, that hosts all those proofs, possibly an on the browser editor, and which all mathematicians in the world use as the one golden reference of mathematics to rule them all!

Just imagine the impact.

Standard library maintainers don't have to deal with the impossible question of what is "beautiful" or "useful" enough mathematics to deserve merged: users just push content to the online database, and star what they like!

We then just use GitHub-like namespaces for each person's theorem, e.g. "cirosantilli/fundmaental-theorem-of-calculus" or "johndoe/fundmaental-theorem-of-calculus" so that each person owns their own preferred definition IDs, which others can reuse.

No more endless bikeshedding over what insane level of generality do your analysis theorems need to be (Ciro Santilli attended at talk about Lean where the speaker mentioned this was a problem)!

This would move things more out of the "pull request and Git tracked code" approach, into a more "database with entries" version of things.

Furthermore, it is just a matter of time until the "single standard library" approach starts to break down, as the git clone becomes impossibly large. At this point, people have to start publishing separate packages. And when this happens, you would need to retest every package that you add to your project. This is why a centralized database is just inevitable at some point, it just scales better.

Interested in a conjecture? No problem: just subscribe to its formal statement + all known equivalents, and get an email on your inbox when it gets proved!

Are you a garage mathematician and have managed to prove a hard theorem, but no "real" mathematician will read your proof because your unknown? Fuck that, just publish it on the system and let it get auto verified. Overnight fame awaits.

Notation incompatibility hell? A thing of the past, just automatically convert to your preferred representation.

Such a system would be the perfect companion to OurBigBook.com. Just like computer code offers the backbone of Linux Kernel Module Cheat Linux kernel tutorials, a formal proof system website would be the backbone of mathematics tutorials! You know what, if OurBigBook.com becomes insanely successful, Ciro is going to add this to it later on.

Furthermore, it would not be too hard to achieve this system!

All we would need would be something analogous to a package registry like PyPI or NodeJS' registry.

Then, each person can publish packages containing proofs.

Packages can rely on other packages that contain pre-requisites definition or theorem.

Packages are just regular git repos, with some metadata. One notable metadata would be a human readable description of the theorems the package provides.

The package registry would then in addition to most package registries have a CI server in it, that checks the correctness of all proofs, generates a web-page showing each theorem.

All proofs can be conditional: the package registry simply shows clearly what axiom set a theorem is based on.

This is a close as we can get to Erdős' book.

Maybe Ciro will just stuff this into OurBigBook.com once that takes over the world.

This project could be seen as a more automated/less moderated version of ProofWiki.

This would be a bit like erdosproblems.com, but with formal proofs. Note for example that Formal Conjectures has formalized these specific problems at: github.com/google-deepmind/formal-conjectures/tree/main/FormalConjectures/ErdosProblems

Bibliography:

Ciro Santilli pinging people:

These are some users Ciro Santilli particularly respects, mostly due to their contributions to systems programming subjects:

Ciro also really likes the following users, a bit less like Gods, and bit more like friends:

Other interesting people:

Bought: November 2023 during Black Friday sale for £1,323.00 to be Ciro Santilli's main personal laptop.

Six years after, and we are 2x on every key spec (except processor Hz ;-) at about 1/2 the price and 1/2 the weight (though smaller 14" screen for greater portability), so not bad! Customized to max out each hardware spec:

Specs:

Identifiers:

Upon arrival:

Buy research:

Log:

2024-01-17: firmware update:Actually fixed performance mode: askubuntu.com/questions/604720/setting-to-high-performance/1343879#1343879

The cartridge is number 33 or 33 XL.

2025-11: moved it around an lost charger cable. Bought new cable www.amazon.co.uk/dp/B08YDJ9N6W "USB 2.0 Type A Male to B" but not turning on using chargers that work for cell phone, so I'm not sure if a charger problem, or if it printer was broken while deplacing it...

2026-02-07: might have lost a the left North Face etip recycled gloves black with white signs, rebuying without too much thinking, redundancy is fine now that I'm old and don't have time: www.amazon.co.uk/dp/B08BDPDNH7

2025-12-28: after losing the Karrimor X Lite Run Black Headband for good going to try a few ones online:

2024-11: OK, I give up, going to try and find the Extremities XDRY again, as these are the perfect gloves for the UK. Buying www.amazon.co.uk/dp/B00OISFUQ4. Their marketing is very confusing and there are several different names for the product, but the label reads "extremities insulated waterpoof sticky power liner glove", black, large. This is the official page: www.terra-nova.co.uk/products/insulated-waterproof-sticky-power-liner-gloves X-Dry Stretch, 100% polyester.

2024-10: going to try Endura Men's Strike Glove - Hi-Viz Yellow, Large www.endurasport.com/strike-glove-hi-viz-yellow/12929542.html | www.wiggle.com/endura-strike-gloves-930526#colcode=93052613. These gloves are high quality, but they are too hot and fleecy for the UK, unless it is an exceptionally cold winter day around 0. This means that they get quite wet from sweat, and they are not that breathable. Also they are very hard to take off and put on, which is painful if you are like me who uses your cell phone for navigation, and while it works with touchscreens, sometimes it's just too annoying and you have to take them off.

2024-05: going to try www.sealskinz.com/products/water-repellent-all-weather-glove Sealskinz Tasburgh Water Repellent All Weather love black large because Extremities XDRY has a hole on right thumb due to gear shifting. This glove is very similar to the Nike academy hyperwam, not really a winter glove feels like. Weird branding...

2023-11: Endura Windchill Bibtights XL - Black: www.endurasport.com/windchill-bibtights-black/12926004.html because knees of dhb one open. I'm an idiot for getting XL... it's just that L felt too short on the top. But ultimately XL was too baggy, this became quite apparent on first usage, L would likely have been better, just would have needed to pull it a bit more. Quality is very good, very water repellent, kept me warm on 2C under very light rain. Also tried www.endurasport.com/xtract-bibtight-black/12926142.html but the sizing was completely different. L on that one as obviously too large, M felt correct.

2023-07: lost my waterproof cap, not cycling specialized, but was useful. Was by itself in crappy backpocket of cheap muddy fox jersey, lots of wind, some fence jumping... Hadn't noted know the brand/model... sad. Let's try Castelli A/C 2 Cycling Cap? www.castelli-cycling.com/US/en/Men/Collection/Hot-Weather-Kit/A-C-2-CYCLING-CAP/p/4523032_008 Single size. Slightly small, but hard to be sure.

2023-07: www.dhbsport.com/products/aeron-short-sleeve-jersey-2-0 dhb Aeron Short Sleeve Jersey 2.0 Colour Ink Blue Size (Standard) L. To prevent crap from falling again hopefully. Felt too small. Material: 100% polyester, inserts, 64% polyester, 6% elastane. Compared to the non 2.0 which I have, the material feels more glossy/slippery. Slightly weird.

2023-05: www.wiggle.com/p/dhb-classic-shorts?color=black&sizeStandard=M dhb Classic Shorts, medium.

2022-05: buying another "dhb Lightweight Mesh Long Sleeve Base Layer", small www.wiggle.com/p/dhb-lightweight-mesh-long-sleeve-base-layer. I notice that it is actually a bit not long enough. Doesn't make a huge difference, but maybe medium or large next time.

2022-12 Rohan Polar Gloves, black, large, 45 pounds. Shell: 85% polyamide, 15% elastane. Insulation: 100% polyester. 100g insulation on back of the hand. www.rohan.co.uk/mens/accessories-polar-gloves Let's see how they perform after hands were very cold on a bike ride with the Extremities XDRY.

2022-08 dhb Aeron Short Finger Gel Gloves 2.0 medium white www.wiggle.co.uk/dhb-aeron-short-finger-gel-gloves-20. For sun/fall protection. In theory should be small according to size guide, but small was over, and I have my doubts it is correct.

2021-12: bought a North Face etip recycled gloves black with white signs, large about 40 dollars: www.thenorthface.co.uk/shop/en-gb/tnf-gb/mens-etip-gloves-4sha?variationId=KY4 let's see how that goes. These ended up being very good. They are not very warm, good for 10-15 C maybe, which is a important range. Water performance is very good

2021-12:

2021-06: Castelli UPF 50+ Light Arm Sleeves (Skins) Large White, 29 pounds www.castelli-cycling.com/bg/upf-50-+-light-arm-sleeves/p/451603621P-001. Felt really good. Really does not trap much heat, and completely blocks off sun. It makes you develop a small layer of sweat that keeps you cool, cooler than without the sleeves.

2021-02 Castelli PRO THERMAL SKULLY red www.wiggle.co.uk/castelli-pro-thermal-skully www.castelli-cycling.com/gb/pro-thermal-skully/p/452054220A to help with cold, the X Lite Run Black Headband is just not made for winter.

2021-01: Madison Cycle Everywear Sportive Toe covers. L/XL. www.madison.cc/shop/sportive-thermal-toe-covers/VARCLA121/CLA12104

2021-01: "Endura FS260-NEMO Glove II" Neoprene Winter Handwarmer Large. www.endurasport.com/Gants-Nemo-FS260-Pro-II/p/E1216-Black Let's see how neoprene feels like. Basically it becomes wet with your transpiration, but is still relatively warm, would take it well down to 5C. Likely would work well with heavy rain. Not bad. But does feel a bit cooler than the Extremities XDRY, especially after you walk for a bit, and your hand becomes cold, and it is very hard to warm it because it is also wet.

2020-12-21: "dhb Neoprene Nylon Overshoes" www.wiggle.co.uk/dhb-neoprene-nylon-overshoes large black. After 2 rides, noticed that the front lower part of left foot (the one I put on and off the most) had a hole in it, not sure where it was made. Edit: I later noticed that it is because I have the reflex of braking slightly with my shoes in certain conditions, e.g. at lower speeds in close proximity to pedestrians, the sounds of which also serve as a way to alert them without the need for a loud bell. But it destroys the overshoe, so I have to undo that reflex.

2020-11-06 www.alpinetrek.co.uk/castelli-perfetto-ros-long-sleeve-cycling-jersey/ "Castelli Perfetto RoS Long Sleeve - Cycling jersey" size L Large. On Wiggle: www.wiggle.co.uk/castelli-perfetto-ros-long-sleeve-jersey Feels great. Together with the dhb Merino Long Sleeve Base Layer, I can gown down to 0 Celcius, no problem, and up to 14 with the "Mesh Long Sleeve Base Layer". Breathes great, blocks wind and rain reasonably, and can holds mild rain out on a short 1.5h ride without problem. I used this so much it is unbelievable.

2020-10-17:

For sizing see also: Ciro Santilli's body.

2020-11: Castelli Thermoflex 2 Arm Warmers, Large, 28 pounds: www.wiggle.co.uk/castelli-thermoflex-2-arm-warmers | www.castelli-cycling.com/gb/men/accessories/cycling-leg-and-arm-warmers/p/451953020A-010 advertized 8°-20°C. Was going to buy the DHB ones for 10 pounds less, but always out of so Castelli it is.

2020-08: started getting getting cold, so let's do it:

2020-05 www.wiggle.co.uk/dhb-aeron-short-sleeve-jersey-4/ dhb Aeron Short Sleeve Jersey 100% polyester, Red Large. This one fit OK. Length feels right. When on cycling position, a bit baggy under arms though, but guessing M would be too short? Still already feels less baggy than the cheap muddy fox jersey. Aeron is the second lowest level of DHB top, after the super basic 25 pound one. Material is thin polyester, could be better, but OK.

2020-05 www.wiggle.co.uk/castelli-perfetto-light-2-short-sleeve-jersey/ Castelli Perfetto Light 2 Short Sleeve Jersey 84% Nylon, 16% Lycra. When it arrived, was WAY too small, so returned. Material looked and felt amazing.

2019-12 www.wiggle.co.uk/dhb-merino-long-sleeve-base-layer-1/?sku=5360752872 "dhb Merino Long Sleeve Base Layer", black, small, was right size, wool is a bit itchy, but does feel like it dries off more quickly on long rides than the cheap Muddy Fox polyester cycling Jersey. Pretty warm, too much for 15C.

2019-12 www.wiggle.co.uk/dhb-aeron-winter-weight-merino-sock/?sku=100335580 dhb Aeron Winter Weight Merino Sock, blue, UK 9.5-12. Did not seem to make much of a difference, feet still cold, not wet.

2019-11 Nike academy hyperwarm gloves: www.nike.com/gb/t/hyperwarm-academy-football-gloves-s9Dd8D/GS0373-013 (archive) for 17.99 Pounds from physical retailer. Good intermediate between the Extremities gloves when it gets a bit warmer. 60% polyester/27% nylon/5% rubber/4% elastane.

2019-10 XGC Men's Cycling Shorts/Bike Shorts And Cycling Underwear With High-Density High-Elasticity And Highly Breathable 4D Sponge Padded www.amazon.co.uk/dp/B07BDJP64W (archive). Grey color, red inner butt padding. 2020-08: after using it a lot, noticed that the padding stiches started to come off a bit.

2018 (?) Extremities XDRY gloves Looks like: www.sportsdirect.com/extremities-wp-p/line-glove-91-907293 (archive) Gets wet after a few minutes of medium rain. But does dry quickly. Baggy, multilayer. Says 40 pounds, but always at 20 pound discount, so it is just a marketing trick. On website: Outershell 96% Polyester/4% Lycra (Spandex)Palm 45% Polyester/55% PolyurethaneLining 100% Polyester

2017-09 Trespass Cruzado Male Gloves size S. www.trespass.com/cruzado-unisex-gloves (archive) Markings: crossover gloves. Technical Performance TP75: www.trespass.com/advice/trespass-tp-ratings-guide/ Lost right hand around 2018/2019.

2017 Muddy fox cycling Jersey, orange, polyester, Large, cheap. Works well enough I guess. Could be a bit more tight fitting.

2017 www.amazon.co.uk/Nevica-Unisex-Reversible-Skuff/dp/B07GSD4R7Y Nevica Skuff black

2017 www.ebay.co.uk/itm/254646634761 Karrimor X Lite Run Black Headband. Had a hole in the ear for a long time. Miraculously surived being almost lost on several occasions, including once it fell off from bike and a dude coming behind pointed it to me. But then alas on 2025-12-28 I lost it, noticed next day wasn't there, by chance found it on neighboring park, but it had been torn very badly, a dog must have done that, so I had to throw it away!

2015 UNIQLO tights 53% cotton, 32% polyester, 15% elastane. 2020-08: after riding it a lot, it ripped a bit near upper inner tights.

2015 Odlo top and tights, polyester. Not sure exact model, not necessarily meant for cycling. Top does not fit tightly, did not feel like it was removing sweat effectively.

Amazing self-directed learning direction:

world.hey.com/gwyn/no-excuses-bc4152fb mentions that the founder was inspired by other schools: High Tech High and Expeditionary Learning.

Lots of focus on showcase student work.

The founder Gwyn ap Harri is quite dirty mouthed, which is also cool.

Ciro Santilli tried to contact them in 2021 at: twitter.com/cirosantilli/status/1448924419016036353 and on website contact form to see if we could do some project together, but no reply.

To be fair, this is one of the least worse ones.

Ciro Santilli controls the following accounts.

With non-trivial activity:

Trivial or no activity:

Profiles without URLs (OMG...):

Lost or deleted:

Accounts in Chinese websites. These accounts might be banned or altered or offer other limitations, so Ciro only communicates briefly through them. All communication through those channels should obviously be assumed to be compromised:

Accounts in Russian websites:

Dead websites:

Ciro Santilli is a UK resident. He will register as a "solo trader" (slightly funny legal term) and treat donations that he uses for projects as grants, which pay regular income tax:The rates are given at: www.gov.uk/income-tax-rates and are as of writing:

National insurance is also likely going to be paid: www.gov.uk/self-employed-national-insurance-rates:

Fortunately however VAT does not need to be paid.

The amount that will be declared is the same as he grant amount that was requested, e.g. if 100k USD is requested for 1 year, then 100k USD will be pro-rata declared on that year.

Any remaining donations that don't yet meet specific grant goals will be initially treated as cash gifts which pay no tax. If in the future they are used as grant money after further goal amounts are reached, then they will taxed as grants.

Note however that if the donor is UK-based and dies within 7 years of the gift being given, inheritance tax has to be paid on them as per: www.gov.uk/inheritance-tax/gifts, at a maximum of 32% and going to to 0% at 7 years, so let me know from the afterlife.

Ciro paid his bill for £24,321.87 ($32,729.70) on 2026-01-02. Announcements:

Source code:

The way Lean and Coq mix programming and mathematics is a thing of great beauty. This is especially notable in lean as you start to play with with things such as:

They are huge fans of Unicode characters! Check this out from a formal proof of the prime number theorem: github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/fbdbb5310d036d33b9797b35f3b04b08f2447a6e/PrimeNumberTheoremAnd/ZetaBounds.lean Here's map to Ascii: proofassistants.stackexchange.com/questions/954/does-lean-have-a-standard-ascii-representation/5289#5289

Their dependency graph thingy is just beautiful however: alexkontorovich.github.io/PrimeNumberTheoremAnd/web/dep_graph_document.html

Their 2025 current installation method is bullshit, recommends VS Code extension on Ubuntu. Lol.

From CLI:Then when you run:it downloads the lean executable for you. Insane shit, could only come from a Microsoft mindset.

A generalization of the Pythagorean triple infinity question.

Evil company that desecrated the beauty created by Sun Microsystems, and was trying to bury Java once and or all in the 2010's.

Their database is already matched by open source e.g. PostgreSQL, and ERP and CRM specific systems are boring.

Oracle basically grew out of selling one of the first SQL implementations in the late 70's, and notably to the United States Government and particularly the CIA. They did deliver a lot of value in those early pre-internet days, but now open source is and will supplant them entirely.

Sets are unordered, but we can use them to create ordered objects, which are of fundamental importance. Notably, they are used in the definition of functions.

The length of its cycle.

Bibliography: