@4bpp's banner p

4bpp

Now I am become a Helpful, Honest and Harmless Assistant, the destroyer of jobs

3 followers   follows 2 users  
joined 2022 September 05 01:50:31 UTC

<3


				
User ID: 355


				
				
				

			

		

	














	


		


			



	

		

			

			

				

					

						

							
						

						

							
							

								
4bpp


								

								

								
								
								

								
							
					
 
				


				
Now I am become a Helpful, Honest and Harmless Assistant, the destroyer of jobs

				
				
				

				

					3 followers  

					follows 2 users  

					joined 2022 September 05 01:50:31 UTC
				


				
					

					
<3



				

				

				

				

				

					

					

					
					
					

					
User ID: 355


					
					
					
				

			


					

						
					



		

	

 











			
			

			
			

			




	


		

			
‎

			

				
				

					Hour
					Day
					
					Month
					Year
					All
				

			


			
‎

			

	
	

	 Hot Bump Top Bottom Old Controversial Comments
	



		

	






	

		
		

		
		
	

	

  







		

			
			
				Culture War Roundup for the week of May 25, 2026
			
		

	

	

	

		
			

			

				

			

		

			


				

					
I still can't make sense of what you are trying to say then. What is the sense in which you claim proofs to be "interchangeable" in classical systems, why do you believe this to be a desirable property, and how do you contend with the fact that constructive proofs are classical proofs?


There may be some HoTT-like sense in which two proofs in a given system are not equivalent (because you introduced some equivalence relation on proofs that does not relate them). If you have a sound embedding from proofs in this system to proofs in another system, and the other system comes with its own equivalence relation on proofs, the images of your two proofs under the embedding might still be equivalent in the other system. Is this not just what would happen here, if you assert that all classical proofs of a given sentence are equivalent (under an equivalence relation you picked) but not all constructive ones are (under an equivalence relation you picked)?




This is doubly-so in cases like cryptography, where almost none of the "incorrectness" of compromised crypto is incorrect at all in the classical mathematical sense.




You will have to elaborate on this statement. What do you take to be an instance of compromised crypto that is not "incorrect in the classical mathematical sense"?


				

				

						

							

								
							

						


						
					

				
			


			

	


			
			
				

			
		

	






		

			
			
				Culture War Roundup for the week of May 25, 2026
			
		

	

	

	

		
			

			

				

			

		

			


				

					
I do not understand where you were trying to go with your digression about constructivism. Is this just supposed to be FUD, as in you hope non-technical readers will look at it and walk away with an understanding like "what Terry produces with his AI is not a real proof"? Because the reality is rather the opposite: any proof in a constructive system like Lean is a proof in a non-constructive system like ZFC, and certainly it is especially a proof in the unspecified system that is mathematical practice outside of a handful of particularly rigorous subfields.


				

				

						

							

								
							

						


						
					

				
			


			

	


			
			
				

			
		

	






		

			
			
				Culture War Roundup for the week of May 25, 2026
			
		

	

	

	

		
			

			

				

			

		

			


				

					


But the most insidious form would be an entire simulated life (or, series of lives) that is always prearranged from the start to have a happy ending.




Have you ever felt, in moments where you suspect that things have gone surprisingly well for you all things considered, that you might already be living such a life?


The timing of the AI takeoff, in our (your?) lifetime, is suspicious too. A genuinely godlike experience machine could surely come up with and colour in any setting (but then its ways would be inscrutable for the simulatees); but a primitive model would probably reach for the normal human life setting that it has the most data on, which is the time just before it was created. "Most non-P-zombie human experiences are reasonably comfortable and fulfilling lives in a threshold world" is an observation that is consistent with an "AI takeover -> brief proliferation of experience machines -> end of conscious life" reality.