Ciro Santilli @cirosantilli 35

 Incoming links: Hacker News

The best articles by Ciro Santilli  Updated 2025-02-22  +Created 1970-01-01

 View more

These are the best articles ever authored by Ciro Santilli, most of them in the format of Stack Overflow answers.

Ciro posts update about new articles on his Twitter accounts.

A chronological list of all articles is also kept at: Section "Updates".

Some random generally less technical in-tree essays will be present at: Section "Essays by Ciro Santilli".

Trended on Hacker News:
- CIA 2010 covert communication websites on 2023-06-11. 190 points, a mild success.
- x86 Bare Metal Examples on 2019-03-19. 513 points. The third time something related to that repo trends. Hacker news people really like that repo!
  - again 2020-06-27 (archive). 200 points, repository traffic jumped from 25 daily unique visitors to 4.6k unique visitors on the day
- How to run a program without an operating system? on 2018-11-26 (archive). 394 points. Covers x86 and ARM
- ELF Hello World Tutorial on 2017-05-17 (archive). 334 points.
- x86 Paging Tutorial on 2017-03-02. Number 1 Google search result for "x86 Paging" in 2017-08. 142 points.
  Figure 1.
  BIOS bare metal hello world running on a Lenovo ThinkPad T430
  . Source.
x86 assembly
- What does "multicore" assembly language look like?
- What is the function of the push / pop instructions used on registers in x86 assembly? Going down to memory spills, register allocation and graph coloring.
Linux kernel
QEMU
gcc and Binutils:
- How do linkers and address relocation works?
- What is incremental linking or partial linking?
- GOLD (-fuse-ld=gold) linker vs the traditional GNU ld and LLVM ldd
- What is the -fPIE option for position-independent executables in GCC and ld? Concrete examples by running program through GDB twice, and an assembly hello world with absolute vs PC relative load.
- How many GCC optimization levels are there?
- Why does GCC create a shared object instead of an executable binary according to file?
C/C++: almost all of those fall into "disassemble all the things" category. Ciro also does "standards dissection" and "a new version of the standard is out" answers, but those are boring:
- What does "static" mean in a C program?
- In C++ source, what is the effect of extern "C"?
- Char array vs Char Pointer in C
- How to compile glibc from source and use it?
- When should static_cast, dynamic_cast, const_cast and reinterpret_cast be used?
- What exactly is std::atomic in C++?. This answer was originally more appropriately entitled "Let's disassemble some stuff", and got three downvotes, so Ciro changed it to a more professional title, and it started getting upvotes. People judge books by their covers.
- notmain.o 0000000000000000 0000000000000017 W MyTemplate<int>::f(int) main.o 0000000000000000 0000000000000017 W MyTemplate<int>::f(int)
  Code 1.
  nm outputs showing that objects are redefined multiple times across files if you don't use template instantiation properly
  . From: What is explicit template instantiation in C++ and when to use it?

IEEE 754

What is difference between quiet NaN and signaling NaN?
In Java, what does NaN mean?

Without subnormals:

          +---+---+-------+---------------+-------------------------------+
exponent  | ? | 0 |   1   |       2       |               3               |
          +---+---+-------+---------------+-------------------------------+
          |   |   |       |               |                               |
          v   v   v       v               v                               v
          -----------------------------------------------------------------
floats    *    **** * * * *   *   *   *   *       *       *       *       *
          -----------------------------------------------------------------
          ^   ^   ^       ^               ^                               ^
          |   |   |       |               |                               |
          0   |   2^-126  2^-125          2^-124                          2^-123
              |
              2^-127

With subnormals:

          +-------+-------+---------------+-------------------------------+
exponent  |   0   |   1   |       2       |               3               |
          +-------+-------+---------------+-------------------------------+
          |       |       |               |                               |
          v       v       v               v                               v
          -----------------------------------------------------------------
floats    * * * * * * * * *   *   *   *   *       *       *       *       *
          -----------------------------------------------------------------
          ^   ^   ^       ^               ^                               ^
          |   |   |       |               |                               |
          0   |   2^-126  2^-125          2^-124                          2^-123
              |
              2^-127

Code 2.

Visualization of subnormal floating point numbers vs what IEEE 754 would look like without them

. From: What is a subnormal floating point number?

Computer science
- Algorithms
  - Figure 5.
    Average insertion time into heaps, binary search tree and hash maps of the C++ standard library
    . Source. From: Heap vs Binary Search Tree (BST)
- Is it necessary for NP problems to be decision problems?
- Polynomial time and exponential time. Answered focusing on the definition of "exponential time".
- What is the smallest Turing machine where it is unknown if it halts or not?. Answer focusing on "blank tape" initial condition only. Large parts of it are summarizing the Busy Beaver Challenge, but some additions were made.

Git

  | 0           | 4            | 8           | C              |
  |-------------|--------------|-------------|----------------|
0 | DIRC        | Version      | File count  | ctime       ...| 0
  | ...         | mtime                      | device         |
2 | inode       | mode         | UID         | GID            | 2
  | File size   | Entry SHA-1                              ...|
4 | ...                        | Flags       | Index SHA-1 ...| 4
  | ...                                                       |

Code 3.

ASCII art depicting the binary file format of the Git index file

. From: What does the git index contain EXACTLY?

tree {tree_sha}
{parents}
author {author_name} <{author_email}> {author_date_seconds} {author_date_timezone}
committer {committer_name} <{committer_email}> {committer_date_seconds} {committer_date_timezone}

{commit message}

Code 4.

Description of the Git commit object binary data structure

. From: What is the file format of a git commit object data structure?

How do I clone a subdirectory only of a Git repository?

Python
- What is the difference between old style and new style classes in Python?
- What is a mixin in Python, and why are they useful?
- What are the differences between threads and processes in Python?
  Figure 6.
  Python Threads vs Processes with 8 hyperthreads
  . Source.
Web technology
- What does enctype='multipart/form-data' mean?
- JavaScript
  - How does JavaScript .prototype work?
  - What is the difference between .prop() vs .attr() in JavaScript?
OpenGL
- Figure 7.
  OpenGL rendering output dumped to a GIF file
  . Source. From: How to use GLUT/OpenGL to render to a file?
- Figure 8.
  Example of a texture atlas containing glyphs
  . Source.
  Image by Nicolas P. Rougier, author of Freetype GL.
  Used on Ciro Santilli's answer: How to draw text using only OpenGL methods?
- Figure 9.
  OpenGL glFrustrum vs glOrtho
  . Source. From: How to use glOrtho() in OpenGL?
- What are shaders in OpenGL?
- Why do we use 4x4 matrices to transform things in 3D?
- Figure 10.
  Sinusoidal circular wave heatmap generated with an OpenGL shader at 60 FPS on SDL
  . Source.
  From: Is it possible to build a heatmap from point data at 60 times per second?
  Compared CPU vs GPU shaders.
- Image Processing with GLSL shaders? Compared the CPU and GPU for a simple blur algorithm.
  Figure 11. Source.
  Video 1.
  OpenGL GPU GLSL fragment shader real time v4l2 Linux webcam computer vision box blur vs CPU
  . Source.
Node.js
- What's the difference between dependencies, devDependencies and peerDependencies in npm package.json file?
Ruby on Rails
- What is the difference between +<%+, +<%=+, +<%#+ and +-%>+ in ERB in Rails?
POSIX
- What is POSIX? Huge classified overview of the most important things that POSIX specifies.

Systems programming

What do the terms "CPU bound" and "I/O bound" mean?
Figure 12.
Plot of "real", "user" and "sys" mean times of the output of time for CPU-bound workload with 8 threads
. Source. From: What do 'real', 'user' and 'sys' mean in the output of time?

+--------+                  +------------+       +------+
| device |>---------------->| function 0 |>----->| BAR0 |
|        |                  |            |       +------+
|        |>------------+    |            |
|        |             |    |            |       +------+
   ...        ...      |    |            |>----->| BAR1 |
|        |             |    |            |       +------+
|        |>--------+   |    |            |
+--------+         |   |         ...        ...    ...
                   |   |    |            |
                   |   |    |            |       +------+
                   |   |    |            |>----->| BAR5 |
                   |   |    +------------+       +------+
                   |   |
                   |   |
                   |   |    +------------+       +------+
                   |   +--->| function 1 |>----->| BAR0 |
                   |        |            |       +------+
                   |        |            |
                   |        |            |       +------+
                   |        |            |>----->| BAR1 |
                   |        |            |       +------+
                   |        |            |
                   |             ...        ...    ...
                   |        |            |
                   |        |            |       +------+
                   |        |            |>----->| BAR5 |
                   |        +------------+       +------+
                   |
                   |
                   |             ...
                   |
                   |
                   |        +------------+       +------+
                   +------->| function 7 |>----->| BAR0 |
                            |            |       +------+
                            |            |
                            |            |       +------+
                            |            |>----->| BAR1 |
                            |            |       +------+
                            |            |
                                 ...        ...    ...
                            |            |
                            |            |       +------+
                            |            |>----->| BAR5 |
                            +------------+       +------+

Code 5.

Logical struture PCIe device, functions and BARs

. From: What is the Base Address Register (BAR) in PCIe?

Electronics
- Raspberry Pi
  - Figure 13.
    Raspberry Pi 2 directly connected to a laptop with an Ethernet cable
    . Image from answer to: How to hook up a Raspberry Pi via Ethernet to a laptop without a router?
    Figure 14.
    Raspberry Pi 2 connected to a laptop with an USB UART adapter
    . Image from answer to: How to hook up a Raspberry Pi via Ethernet to a laptop without a router?
    Figure 15.
    Raspberry Pi OS being emulated on QEMU 2.5.0 on Ubuntu 16.04 with a modified kernel
    . Image from answer to: How to emulate the Raspberry Pi 2 on QEMU?
    Figure 16.
    Bare metal LED blinker program running on a Raspberry Pi 2
    . Image from answer to: How to run a C program with no OS on the Raspberry Pi?
Computer security
- Why is the same origin policy so important?
Media
- Video 2.
  Canon in D in C
  . Source.
  From: How is audio represented with numbers in computers?.
  The original question was deleted, lol...: How to programmatically synthesize music?
- How to resize a picture using ffmpeg's sws_scale()?
- Is there any decent speech recognition software for Linux? ran a few examples manually on vosk-api and compared to ground truth.
Eclipse
- How to set up the Eclipse for remote C debugging with gdbserver?
Computer hardware
- Are there good open source standard cell libraries to learn IC synthesis with EDA tools?
Scientific visualization software
- Figure 17.
  VisIt zoom in 10 million straight line plot with some manually marked points
  . Source. From: Section "Survey of open source interactive plotting software with a 10 million point scatter plot benchmark by Ciro Santilli"
Numerical analysis
- Video 3.
  Real-time heat equation OpenGL visualization with interactive mouse cursor using relaxation method by Ciro Santilli (2016)
  Source.
Computational physics
- Figure 18.
  gnuplot plot of the y position of a sphere bouncing on a plane simulated in Bullet Physics
  . Source. From: What is the simplest collision example possible in a Bullet Physics simulation?
Register transfer level languages like Verilog and VHDL
- Verilog:
  Figure 19.
  Interacgive ASDF-controlled demo with core logic written in Verilog using Verilator
  .
  From: Is it possible to do interactive user input and output simulation in VHDL or Verilog?
  See also: Section "Verilator interactive example"
Android
- Figure 20. Source. From: How to compile the Android AOSP kernel and test it with the Android Emulator?
- Video 4.
  Android screen showing live on an Ubuntu laptop through ADB
  . Source. From: How to see the Android screen live on an Ubuntu desktop through ADB?
Debugging
Program optimization
- What is tail call optimization?
- Figure 21.
  gprof2dot image generated from the gprof data of a simple test program
  . Source.
  From: How can I profile C++ code running on Linux?
  The answer compares gprof, valgrind callgrind, perf and gperftools on a single simple executable.
Data
- Figure 22.
  Mathematics dump of Wikipedia CatTree
  . Source.
Mathematics
- Figure 23.
  Diagram of the fundamental theorem on homomorphisms by Ciro Santilli (2020)
  
  Shows the relationship between group homomorphisms and normal subgroups.
  From: What is the intuition behind normal subgroups?
- Section "Formalization of mathematics": some early thoughts that could be expanded. Ciro almost had a stroke when he understood this stuff in his teens.
- Figure 24.
  Simple example of the Discrete Fourier transform
  . Source. That was missing from Wikipedia page: en.wikipedia.org/wiki/Discrete_Fourier_transform!
Network programming
- How to make an HTTP get request in C without libcurl?
Physics
- What is the difference between plutonium and uranium?
- Figure 25.
  Spacetime diagram illustrating how faster-than-light travel implies time travel
  . From: Does faster than light travel imply travelling back in time?
Biology
- Figure 26.
  Top view of an open Oxford Nanopore MinION
  . Source. From: Section "How to use an Oxford Nanopore MinION to extract DNA from river water and determine which bacteria live in it"
- Figure 27.
  Mass fractions in a minimal growth medium vs an amino acid cut in a simulation of the E. Coli Whole Cell Model by Covert Lab
  . Source. From: Section "E. Coli Whole Cell Model by Covert Lab"
Quantum computing
- Section "Quantum computing is just matrix multiplication"
- Figure 28.
  Visualization of the continuous deformation of states as we walk around the Bloch sphere represented as photon polarization arrows
  . From: Understanding the Bloch sphere.
Bitcoin
- Section "Cool data embedded in the Bitcoin blockchain"
GIMP
- Figure 29.
  GIMP screenshot part of how to combine two images side-by-side in GIMP?
  .
Home DIY
- Figure 30.
  Total_Blackout_Cassette_Roller_Blind_With_Curtains.
  Source. From: Section "How to blackout your window without drilling"
China
- What would happen if I walked around Beijing with a t-shirt that said "freedom of speech is pretty great"?

 Read the full article

USA spying on its own allies  Updated 2025-02-22  +Created 1970-01-01

 View more

Being Brazilian, Ciro Santilli is particularly curious about the existence of a Brazilian-focused website one mentioned in the article, as well as in other democracies.

WTF the CIA was doing in Brazil in the early 2010s! Wasn't helping to install the Military dictatorship in Brazil enough!

Here are the democracies found so far, defining a democracy as a country with score 7.0 or more in the Democracy index 2010. In native language:

Germany(2: dedrickonline.com, neighbour-news.com)
France (4: guide-daventure.com, lesummumdelafinance.com, football-de-luxe.com, suparakuvi.com)
Italy (2: attivitaestremi.com, podisticamondiale.com)
Spain (2: armashoy.com, montanismoaventura.com)
Brazil (1: noticiasmusica.net)
South Korea (1: economicnewsbuzz.com)
Poland (1: boxingstop.net)

In English, so more deniable:

Japan (1: snapnewsfront.net)
Canada (2: kanata-news.com, mynewscheck.com)
Philippines (1: half-court.net)
India (1: amishkanews.com)

"Almost democracies":

Ciro couldn't help but feel as if looking through the Eyes of Sauron himself!

It is worth noting that democracies represent just a small minority of the websites found. The Middle East, and Spanish language sites (presumably for Venezuela + war on drugs countries?) where the huge majority. But Americans have to understand that democracies have to work together and build mutual trust, and not spy on one another. Even some of the enlightened people from Hacker News seem to not grasp this point. The USA cannot single handedly maintain world order as it once could. Collaboration based on trust is the only way.

Snowden's 2013 revelations particularly shocked USA allies with the fact that they were being spied upon, and as of the 2020's, everybody knows this and has "stopped caring", and or moved to end-to-end encryption by default. This is beautifully illustrated in the Snowden when Snowden talks about his time in Japan working for Dell as an undercover NSA operative:

NSA wanted to impress the Japanese. Show them our reach. They loved the live video from drones. This is Pakistan right now [video shows CIA agents demonstrating drone footage to Japanese officials]. They were not as excited about that we wanted their help to spy on the Japanese population. They said it was against their laws.
We bugged the country anyway, of course.
And we did not stop there. Once we had their communications we continued with the physical infrastructure. We sneaked into small programs in their power grids, dams, hospitals. The idea was that if Japan one day was not our allies we could turn off the lights.
And it was not just Japan. We planted software in Mexico, Germany, Brazil, Austria.
China, I can understand. Or Russia or Iran. Venezuela, okay.
But Austria? [shows footage of cow on an idyllic Alpine mountain grazing field, suggesting that there is nothing in Austria to spy on]

Another noteworthy scene from that movie is Video "Aptitude test scene from the Snowden 2016 film", where a bunch of new CIA recruits are told that:

Each of you is going to build a covert communications network in your home city [i.e. their fictitious foreign target location written on each person's desk, not necessarily where they were actually born], you're going to deploy it, backup your site, destroy it, and restore it again.

 Read the full article

Incoming links  Updated 2025-02-22  +Created 1970-01-01

 View more

By Ciro Santilli:

2021-04-13 twitter.com/cirosantilli/status/1382067162492366854: main initial announcement on Twitter. twitter.com/mikko, who has 209.9K followers and a Wikipedia page: Mikko Hypponen hearted the tweet s2
2023-01-21 twitter.com/cirosantilli/status/1749172304259535063: improvements to the Prayer wars
2024-02-07 twitter.com/cirosantilli/status/1755378931446739373: large-ish update with new items and improved organization
2024-03-31 twitter.com/cirosantilli/status/1774531934305071295: binwalk discoveries, start poking a bit into ordinal ruleset inscriptions
2024-04-04 twitter.com/cirosantilli/status/1775805941885108392: largest text ordinal inscription

By others:

2021-04-15 news.ycombinator.com/item?id=26801067 (96 points) on Hacker News. Reached position 16 at one point: archive.ph/L0Fte and led to about 5k views total. Ah, Ciro could watch that Google Analytics realtime view go bling all day long. Narcissism is a bitch.
2021 cryptonewmedia.press/tankman-image-on-bitcoin-blockchain/ by user igadjeed
2022-01-23 news.ycombinator.com/item?id=30050479 "Abuse and Harassment on the Blockchain ", comment-mid thread
2022-01-24 www.reddit.com/r/Buttcoin/comments/sbw0se/when_i_heard_about_nfts_i_thought_they_were/hu2uk8g "When I heard about NFTs, I thought they were stupid, but then I watched a video explaining how they work, it really changed my perspective", comment mid-thread
2023-02 lots of Twitter backlinks as a result of ordinal ruleset inscriptions:
- 2023-02-03
  Video 1.
  Bitcoin= Free Speech Repository? by Trader University (2023)
  Source. Features Marijuana plant and Rickrolling sections. He seems to be a finance guru.
- 2023-02-07 twitter.com/privateid_ntity/status/1622814063331004421
2024-01-18 twitter.com/pete_rizzo_/status/1748049913286447355 by Rizzo, The Bitcoin Historian (81k followers, mid-thread)
2024-12-29: x.com/lopp/status/1873453363523932630 by Jameson Lopp (492k subscribers)
? cloudhiker.net/ A hand curated and categorized list of interesting links by Kevin Woblick. Only allows users to visit a random one per category, so we can't get proof of backlink, this was noticed through Google Analytics.

 Read the full article

Creator of Archive.today  Updated 2025-02-22  +Created 1970-01-01

 View more

drive.google.com/file/d/1JTPVd09NPaGH-KzGv2jU3XXcFiJAoUjw/view some crazy due investigating, let's see how long until it goes down, posted at:
- www.reddit.com/r/COPYRIGHT/comments/1bcqf3y/archivetoday_archiveis_copyright_victims/
- webapps.stackexchange.com/questions/145817/on-which-country-are-the-creators-and-servers-of-archive-today-archive-is-base/175600#175600
Points to:
- www.linkedin.com/in/denispetrov/
"Alex Conferno" is also brought up: twitter.com/conferno
www.reddit.com/r/DataHoarder/comments/12trawt/has_anyone_ever_actually_spoken_to_denis_petrov/
gyrovague.com/2023/08/05/archive-today-on-the-trail-of-the-mysterious-guerrilla-archivist-of-the-internet/. Trended on Hacker News: news.ycombinator.com/item?id=37009598
gigazine.net/gsc_news/en/20240326-archive-today/

Other mentions of "Denis Petrov":

webmasters.stackexchange.com/questions/88257/deny-access-to-archive-is

 Read the full article

Facebook profile face dump  Updated 2025-02-22  +Created 1970-01-01

 View more

In 2016 Ciro made a script downloaded Facebook profile pictures.

This was possible at the time without any login by using a 2010 profile ID dump from originally announced at: blog.skullsecurity.org/2010/return-of-the-facebook-snatchers since profile picture access was not authenticated.

The profile ID dump was downloadable through a BitTorrent named fbdata.torrent of about 2.8GB, mostly compressed. Doing:

find . -type f | xargs sha256sum | sha256sum

on Ubuntu 20.04 gives:

2c9a739c9c5495e38ebab81fc67411b7c6562f139dcb8619901a3f01230efdd5

This dump widely reported e.g. on Hacker News at: news.ycombinator.com/item?id=1554558.

At some point however, Facebook finally started to require tokens to view public profile pictures, thus making such further collection impossible, e.g. as of 2021: developers.facebook.com/docs/graph-api/reference/v9.0/user/picture mentions:

Querying a User ID (UID) now requires an access token.

This is also mentioned e.g. at: stackoverflow.com/questions/11442442/get-user-profile-picture-by-id. This major privacy flaw was therefore finally addressed at some point, making it impossible to reproduce this project.

Ciro downloaded 10 thousand of those pictures, and did facial extraction with: stackoverflow.com/questions/13211745/detect-face-then-autocrop-pictures/37501314#37501314

He then created single a video by joining 10 thousand of those cropped faces which can be uploaded e.g. to YouTube. Ciro later decided it was better to make those videos private however, as sooner later he'd lose his account for it.

Companies like YouTube blocking this kind of content is the type of thing that makes companies take longer to fix such gaping privacy issues, and is a bit like security through obscurity. A video makes it clear to everyone that there is a privacy issue very effectively. But people prefer to hide and look away, and then 99% of people who know nothing about tech get their privacy busted by actual criminals/government spies and never learn about it.

But now that Facebook finally fixed it, it's fine, no need for the video anymore.

 Read the full article

Reactions to cirosantilli.com  Updated 2025-02-22  +Created 1970-01-01

 View more

Deep psychological analyses:

Hacker News user MichaelZuo comments on a post about CIA 2010 covert communication websites:
Yeah [the website] seems a bit odd, as if the author is intentionally trolling in some areas, or is easily susceptible to being trolled by random folks, and thus displaying some kind of compensation dynamic.
www.reddit.com/r/China_irl/comments/1bn47e5/comment/kwgkl88/ user Opening_Gazelle_1323 comments:
Can your kid be the next Fields Medalist or Nobel Prize winner? I'm here to help, especially if you are filthy rich!
三西猴老哥这一张嘴⏰味拉满，可以封为荣誉中国人
Brother Sanxihou’s mouth is so full of flavor that he can be named an honorary Chinese.
www.reddit.com/r/Monero/comments/1brryao/ciro_santilli_received_a_1000_xmr_donation_to/ from 1000 Monero donation user Inaeipathy:;
It reads like an ode to himself, very strange in my opinion. I don't really know what's up with the black-green text scheme, I can barely read any of it.
archive.is/W1ocv originally boards.4channel.org/g/thread/75097729/who-is-this-guy on 4chan:
a based retard
Is that his own personal site where he has just listed everything he has ever done? Based.
He refers to himself in the third person, because gender has non place in the Sciences. Based autismo.
Holy based. Keep up the good work my man.

 Read the full article

The Math Genome Project  Updated 2025-02-22  +Created 1970-01-01

 View more

www.themathgenome.com/

The website was dead as of February 2025. Last archive: web.archive.org/web/20240418004442/http://www.themathgenome.com/ Pings:

x.com/cirosantilli/status/1890873216551313861

They were seeking help on May 2024:

so its likely the followup death. LinkedIn post gives basic stack: MERN stack, Heroku, Supabase/MongoDB Atlas.

Appears to support multiple proof assistant backends including Lean, Hol and Coq.

A discussion on the Lean Zulip: leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20Math.20Genome.20Project/near/352639129. Lean people are not convinced about the model in general it seems however.

TODO closed source? Really? www.themathgenome.com/pricing

TODO not viewable without login?

Has conjectures feature.

Built by this dude John Mercer:

He must be independently wealthy or something to do such a project? What a hero. But he seems to have jobs. On the side? Hardcore.

A failed Hacker News self post: news.ycombinator.com/item?id=35775071

Ciro Santilli asked: discord.com/channels/1096393420408360989/1096393420408360996/1137047842159079474

Does the website actually automatically check the formal proofs, or is this intended to be implemented at some point? And if yes, is it intended to allow proofs to depend on other proofs of the website (possibly by other people)

Owner:

Hi Ciro, yes we will be releasing in-browser proof assistant environments/checkers (e.g. Lean). Our goal is not to replace the underlying open-source repos (e.g. Mathlib) so the main dependency will be on the current repos; then when statement formalizations and proofs come in and are certified they can be PR'd to the respective repos. So we will be the source of truth for the informal latex code but only a stepping stone and orchestration layer on the way to the respective formal libraries.

So apparently there will be proof checking, but nodependencies between proofs, you still have to pull request everywhing back and face the pain.

Bibliography:

 Read the full article