@Soteriologian's banner p

Soteriologian

Unstammering Papageno

1 follower   follows 0 users  
joined 2023 June 30 23:52:08 UTC

Lo, those who are entombed are cast on high grounds.

Men stir up strife unopposed.

Groaning is throughout the land, mingled with laments.

See now the land is deprived of kingship.

What the pyramid hid is empty.

The people are diminished.

-Ipuwer


				
User ID: 2538


				
				
				

			

		

	














	


		


			



	

		

			

			

				

					

						

							
						

						

							
							

								
Soteriologian


								

								

								
								
								

								
							
					
 
				


				
Unstammering Papageno

				
				
				

				

					1 follower  

					follows 0 users  

					joined 2023 June 30 23:52:08 UTC
				


				
					

					
Lo, those who are entombed are cast on high grounds.


Men stir up strife unopposed.


Groaning is throughout the land, mingled with laments.


See now the land is deprived of kingship.


What the pyramid hid is empty.


The people are diminished.


-Ipuwer



				

				

				

				

				

					

					

					
					
					

					
User ID: 2538


					
					
					
				

			


					

						
					



		

	

 











			
			

			
			

			




	


		

			
‎

			

				
				

					Hour
					Day
					Week
					
					Year
					All
				

			


			
‎

			

	
	

	 Hot Bump Top Bottom Old Controversial Comments
	



		

	






	

		
		

		
		
	

	

  







		

			
			
				Culture War Roundup for the week of September 7, 2026
			
		

	

	

	

		
			

			

				

			

		

			


				

					
For reference, the Lean 4 mathlib library is an attempt to formalise all mathematics known to humankind, and it sits at 15M lines.


				

				

						

							

								
							

						


						
					

				
			


			
			
			
				

			
		

	






		

			
			
				Culture War Roundup for the week of September 7, 2026
			
		

	

	

	

		
			

			

				

			

		

			


				

					
Uh, I don’t think so? As far as I remember, the guy was showing off his proof and even used two different provers to make sure his proof was really true and not due to a spurious bug (and he ended up finding two different bugs in two different provers lol)


Where are you hearing that he was merely bug hunting and dressed up his bug as a Collatz proof?


				

				

						

							

								
							

						


						
					

				
			


			
			
			
				

			
		

	






		

			
			
				Culture War Roundup for the week of September 7, 2026
			
		

	

	

	

		
			

			

				

			

		

			


				

					
May be tossing egg on my face, but I'll post this anyway:


There's a decent chance this proof is not valid. It's formalised in Lean 4, yes, but we also had a Lean-verified proof of the Collatz conjecture a couple months ago that turned out to be spurious (they didn't actually find a proof; they found a bug in Lean).


That proof was 320 lines. This Navier-Stokes proof is 1.6 million lines, and according to their README, requires 100GB to even check. Thanks to somebody eating all the ram, my PC does not presently have 100GB, so I can't run Lean myself to check it. But I will point out that the README explicitly mentions Lean 4.32.2, and the release notes for Lean 4.33.1 mention two soundness bugs fixed, so... it sure looks like there are exploitable soundness bugs in the version they used for this proof.


And if an LLM can find a soundness bug in 320 lines, surely it can sneak one into 1.6 million lines.


				

				

						

							

								
							

						


						
					

				
			


			
			
			
				

			
		

	






		

			
			
				Culture War Roundup for the week of August 31, 2026
			
		

	

	

	

		
			

			

				

			

		

			


				

					
Gotta say I agree with the bad writing part. I started reading Foundation a few months ago and couldn't get into it, and haven't bothered trying to finish. Really expected more given how prominent the series is. It reads like rationalist fanfic.