What if the AI lean proofs are syntactically correct but semantically gibberish?Mathematics is a language to describe phenomena, saying "the color seven melts when near furious ideas" is correct but doesn't convey proper information.The AI slop seems to be just marketing to dig them out of the debt hole.
>>17083611>What if the AI lean proofs are syntactically correct but semantically gibberish?Most of them are built on top of human-written formalizations of human mathematical concepts so that is not the case.>saying "the color seven melts when near furious ideas" is correct No, it isn't.
>>17083618>mostnice try migger
thats your kid nigga. im out
>>17083611>What if the AI lean proofs are syntactically correct but semantically gibberish?What do you mean by “what if?”? They are.>my code compilesBut what does it do?>it compiles!Welcome to AI proofs.
>>17083618>No, it isn't.It is grammatically correct
>>17083950>It is grammatically correctYeah but it's a bunch of category errors - one of the most basic mistakes static types help you avoid.
>>17083954You are not able to show that in Lean, are you?
>>17083980Lean proofs are actually programs and the verification is actually type checking. If you've ever used a statically typed programming language, you should have some idea of how types are used to encode semantic properties. If you imagine a program equivalent of the nonsense sentence you wrote, it wouldn't pass a basic type check (7 is not an instance of the `Color` type, the `melt` function is not applicable to `Color`, `Color` doesn't have a `position` property so you can't compare distances etc.). Lean uses dependent types, which vastly extend what semantics you can encode.I understand babby's cope but it's just wrong.
>>17083986>copeTold you he couldn’t do it.>babbyPergtant? Comgwatulate!
>>17083989>babby gets filtered and goes googoo gaaagaa
>>17083991>i can’t
>>17084016>angry babby gurgling noisesCan't what? What are you even on about at this point?
>>17084017>Can't what?>>17083980>>17083989>>17084016And we will add “read” and “retain” to the list.I added “spell” before.And Lean.
>>17084023Are you retarded or what? I've already explained to you how you can prevent such nonsense in Lean. You just need to define the terms.
>>17083986>Lean uses dependent types, which vastly extend what semantics you can encode.Not to arbitrary extents, and there are plenty of problems with viewing types as semantic properties. Type theory has never advocated for any of what you're suggesting.Generally speaking, semantics are orthogonal to formalism. They don't mix at all. His question is completely valid and the answer to it is "we don't know yet".
>>17084037>retarded pseudmumblingShit board full of retards who don't know anything about anything and can't comprehend what they're reading.
>>17084037>there are plenty of problems with viewing types as semantic propertiesname one
>>17084054He literally can't.
>>17084054write me a program which decides through type checking if an arbitrary finitely presented group is trivial.types are classification groupings, not interpretative machinery. you can change the latter without touching anything to do with the former, they're completely disjoint.
>>17084164>write me a program which decides through type checking if an arbitrary finitely presented group is trivial.why would i need to do that? notice your blood pressure rising as you realize you can't provide a coherent answer
>>17083618>Most of them are built on top of human-written formalizations of human mathematical concepts so that is not the case.what if the AI found bugs in lean so it shows it's correct proof but it was actually a bug humans don't even understand because it's that fucking complex?we reached the point where we worship the AI sacred texts without even understanding them
>>17084175>what if the AI found bugs in leanWhat's that got to do with the thread?
>>17083611>Mathematics is a languageIt's not, it's a lot of different languages that use a lot of the same symbols to mean a lot of different things depending on what language you're writing in.
>>17084164>write me a program which decides if an arbitrary finitely presented group is trivialNo program does this. Now, what do you think this proves, brainlette?>types are classification groupings, not interpretative machinery. you can change the latter without touching anything to do with the former, they're completely disjoint.This is just word salad and you're obviously low-IQ.
>>17084167the point that flew over your head is that you cannot, and not just because you're ignorant on what any of those words mean. you can't do it because it's logically impossible.
>>17084199>you cannotand? notice how you will once again fail to respond coherently
>>17084200disproving the notion that types are isomorphic with semantic properties, as you cannot encode this semantic property with even the most expressive form of martin-lof types.
>>17084201>prove that a false statement is true>if you can't do this that means the statement can't be expressedyou're obviously mentally ill
sometimes i stop browsing /sci/ for a while and i forget how fun it is to make the half-wit schizos shit themselves
>>17084202He obviously is and you're still trying to argue with him so what does that say about you?
>>17084203>boiling with impotent ragei'm sure your imaginary audience sympathizes
>>17084202What does that have to do with what he said?
>>17084218it's what you get when you apply the curry-howard correspondence to his delusional mumbling. in the context of dependent types, programs are proofs. so what is the program he's asking for a proof of? that the triviality of arbitrary finitely presented groups is decidable. since that's not the case, he's asking for a proof of a false statement.now, that doesn't prevent you from constructing a type for it. but if you do it correctly, any program with that type annotation will fail to type-check, demonstrating that the type correctly captures the relevant semantics. in short, he's a mentally ill retard spewing word salad
