| |
| ▲ | almostgotcaught 2 days ago | parent | next [-] | | > You say that like it’s even remotely feasible at the frontier of mathematics and not a monumental group effort to turn even established proofs into such. people on hn love making these kinds of declarative statements (the one you responded to, not yours itself) - "for X just do Y" as a kind of dunk on the implied author they're responding to (as if anyone asked them to begin with). they absolutely always grossly exaggerate/underestimate/misrepresent the relevance/value/efficacy of Y for X. usually these declarative statements briskly follow some other post on the frontpage. i work on GPU/AI/compilers and the number of times i'm compelled to say to people on here "do you have any idea how painful/pointless/unnecessary it is to use Y for X?" is embarrassing (for hn). i really don't get even get it - no one can see your number of "likes". twitter i get - fb i get - etc but what are even the incentives for making shit up on here. | | |
| ▲ | nospice 2 days ago | parent | next [-] | | It feels good to be smarter than everyone else. You see your upvotes and that's good enough for an ego boost. Been there, done that. I wish we were a bit more self-critical about this, but it's a tough problem when what brings the community together in the first place is a sense of superiority: prestigious schools, high salaries, impressive employers, supposedly refined tastes. We're at the top of the world, right? | | |
| ▲ | rjh29 2 days ago | parent | next [-] | | HN is frequently fodder for satire on other forums. Nobody thinks HN users have "refined tastes", or even that they are "smart" for that matter. | | |
| ▲ | falseprofit 20 hours ago | parent [-] | | Hey, do you mind sharing any of these other forums? I’m trying to make my way up the satire food chain. |
| |
| ▲ | le-mark 2 days ago | parent | prev [-] | | > prestigious schools, high salaries, impressive employers, supposedly refined tastes. We're at the top of the world, right? Being pompous and self obsessed requires none of those things. | | |
| ▲ | chroma205 2 days ago | parent [-] | | > Being pompous and self obsessed requires none of those things. Sufficient, but not necessary |
|
| |
| ▲ | hexaga 2 days ago | parent | prev | next [-] | | Do selection dynamics require awareness of incentives? I would think that the incentives merely have to exist, not be known. On HN, that might be as simple as display sort order -- highly engaging comments bubble up to the top, and being at the top, receive more attention in turn. The highly fit extremes are -- I think -- always going to be hyper-specialized to exploit the environment. In a way, they tell you more about the environment than whatever their content ostensibly is. | | |
| ▲ | DoctorOetker 2 days ago | parent [-] | | isn't it sufficient of an explanation that one has occasionally wasted a ton of time trying to read an article only to discover after studying and interpreting half of a paper that one of the author's proof steps is wholly unjustified? is it so hard to understand that after a few such events, you wish for authors to check their own work by formalizing it, saving countless hours for your readers, by selecting your paper WITH machine readable proof versus another author's paper without a machine readable proof? | | |
| ▲ | hexaga 2 days ago | parent [-] | | If wishes were fishes, as they say. To demonstrate with another example: "Gee, dying sucks. It's 2025, have you considered just living forever?" To this, one might attempt to justify: "Isn't it sufficient that dying sucks a lot? Is it so hard to understand that having seen people die, I really don't want to do that? It really really sucks!", to which could be replied: "It doesn't matter that it sucks, because that doesn't make it any easier to avoid." | | |
| ▲ | guerrilla 2 days ago | parent | next [-] | | I understand where you're coming from but it's a bad analogy. Formal proofs are extremely difficult but possible. Immortality is impossible. | | |
| ▲ | hexaga 2 days ago | parent [-] | | I don't think it matters, to be quite honest. Absolute tractability isn't relevant to what the analogy illustrates (that reality doesn't bend to whims). Consider: - Locating water doesn't become more tractable because you are thirsty. - Popping a balloon doesn't become more tractable because you like the sound. - Readjusting my seat height doesn't become more tractable because it's uncomfortable. The specific example I chose was for the purpose of being evocative, but is still precisely correct in providing an example of: presenting a wish for X as evidence of tractability of X is silly. I object to any argument of the form: "Oh, but this wish is a medium wish and you're talking about a large wish. Totally different." I hold that my position holds in the presence of small, medium, _or_ large wishes. For any kind of wish you'd like! | | |
| ▲ | guerrilla 2 days ago | parent [-] | | Those are all better analogies than the original one you gave, which didn't illustrate your as clearly as they do. | | |
| ▲ | hexaga a day ago | parent [-] | | Unavoidable: expecting someone else to do the connection isn't a viable strategy in semi-adversarial conditions so it has to be bound into the local context, which costs clarity: - Escaping death doesn't become more tractable because you don't want to die. This is trivially 'willfully misunderstood', whereas my original framing is more difficult -- you'd need to ignore the parallel with the root level comment, the parallel with the conversation structure thus far, etc. Less clear, but more defensible. It's harder to plausibly say it is something it is not, and harder to plausibly take it to mean a position I don't hold (as I do basically think that requiring formalized proofs is a _practically_ impossible ask). By your own reckoning, you understood it regardless. It did the job. It does demonstrate my original original point though, which is that messages under optimization reflect environmental pressures in addition to their content. |
|
|
| |
| ▲ | DoctorOetker a day ago | parent | prev [-] | | wishes can be converted to incentives, what if the incentives change such that formally verified proofs were rewarded more and informal "proofs" less? |
|
|
| |
| ▲ | DoctorOetker 2 days ago | parent | prev [-] | | I grossly underestimate the value of the time of highly educated people having to decode the arguments of another expert? Consider all the time saved if for each theorem proof pair, the proof was machine readable, you could let your computer verify the proclaimed proof as a precondition on studying it. That would save a lot of people a lot of time, and its not random peoples time saved, its highly educated peoples time being saved. That would allow much more novel research to happen with the same amount of expert-years. If population of planet A would use formal verification, and planet B refuses to, which planet do you predict will evolve faster | | |
| ▲ | btilly 2 days ago | parent [-] | | You appear to be deliberately ignoring the point. Currently, in 2025, it is not possible in most fields for a random expert to produce a machine checked proof. The work of everyone in the field coming together to create a machine checked proof is also more work for than for the whole field to learn an important result in the traditional way. This is a fixable problem. People are working hard on building up a big library of checked proofs, to serve as building blocks. We're working on having LLMs read a paper, and fill out a template for that machine checked proof, to greatly reduce the work. In fields where the libraries are built up, this is invaluable. But as a general vision of how people should be expected to work? This is more 2035, or maybe 2045, than 2025. That future is visible, but isn't here. | | |
| ▲ | DoctorOetker 2 days ago | parent [-] | | It's interesting that you place it 10 or 20 years from now, given that MetaMath's initial release was... 20 years ago! So it's not really about the planets not being in the right positions yet. The roman empire lasted for centuries. If they wanted to do rigorous science, they could have built cars, helicopters, ... But they didn't (in Rome, do as the Romans do). This is not about the planets not being in the right position, but about Romans in Rome. | | |
| ▲ | btilly 2 days ago | parent [-] | | Let's see. I could believe you, an internet stranger. And believe that this problem was effectively solved 20 years ago. Or I could read Terry Tao's https://terrytao.wordpress.com/wp-content/uploads/2024/03/ma... and believe his experience that creating a machine checkable version of an informal proof currently takes something like 20x the work. And the machine checkable version can't just reference the existing literature, because most of that isn't in machine checkable form either. I'm going with the guy who is considered one of the greatest living mathematicians. There is an awful lot that goes into creating a machine checkable proof ecosystem, and the file format isn't the hard bit. | | |
| ▲ | DoctorOetker a day ago | parent [-] | | 20x the work of what? the work of staying vague? there is no upper limit to the "work" savings, why not be 5 times vaguer, then formal verification can be claimed to be 100x more work. If ultimate readership (over all future) were less than 20 per theorem, or whatever the vagueness factor would be, the current paradigm would be fine. If ultimate readership (not citation count) were higher than 20 per theorem, its a net societal loss to have the readers guess what the actual proof is, its collectively less effort for the author to formalize the theorem than it would be to have the readers guess the actual proof. As mathematicians both read and author proofs, they would save themselves time, or would be able to move the frontier of mathematics faster. From a taxpayer perspective, we should precondition mathematics funding (not publication) on machine readable proofs, this doesn't mean every mathematician would have to do it, if some hypothetical person had crazy good intuitions, and the rate of results high enough this person could hire people to formalize it for them, to meet the precondition. As long as the results are successfully formalized, this team could continue producing mathematics. |
|
|
|
|
| |
| ▲ | bmitc 2 days ago | parent | prev | next [-] | | Plus, mathematics isn't just a giant machine of deductive statements. And the proof checking systems are in their infant stages and require huge amounts of efforts even for simple things. | | |
| ▲ | sublinear 2 days ago | parent | next [-] | | > mathematics isn't just a giant machine of deductive statements I know HN can be volatile sometimes, but I sincerely want to hear more about these parts of math that are not pure deductive reasoning. Do you just mean that we must assume something to get the ball rolling, or what? | | |
| ▲ | crazygringo 2 days ago | parent | next [-] | | I think the point was that it's not a machine. Stuff that we can deduce in math with common sense, geometric intuition, etc. can be incredibly difficult to formalize so that a machine can do it. | | |
| ▲ | DoctorOetker 2 days ago | parent [-] | | What do you mean with "do it" in "...etc. can be incredibly difficult to formalize so that a machine can do it." ? 1. do it = search for a proof 2. do it = verify a purported proof? | | |
| ▲ | crazygringo 2 days ago | parent [-] | | Deduce. So your #2. | | |
| ▲ | DoctorOetker 2 days ago | parent [-] | | Of course a machine can verify each step of a proof, but that formal proof must be first presented to the machine. | | |
| ▲ | crazygringo 2 days ago | parent [-] | | Right. And I said it's incredibly difficult to formalize so that a machine can do it. I don't understand what you're confused about. | | |
| ▲ | DoctorOetker 2 days ago | parent [-] | | Theres nothing difficult about formalizing a proof you understand. Formalizing hot garbage supposedly describing a proof can be arbitrarily difficult. The problem is not a missing library. The number of definitions and lemmas indirectly used is often not that much. Most of the time wasted when formalizing is discovering time and time again that prior authors are wasting your time, sometimes with verifiably false assumptions, but the community keeps sending you around to another gap-filling approach. | | |
| ▲ | crazygringo 2 days ago | parent [-] | | > Theres nothing difficult about formalizing a proof you understand. What are you basing that on? It's completely false. If that were true, we would have machine proofs of basically everything we have published proofs for. Every published mathematical paper would be accompanied by with its machine-provable version. But it's not, because the kind of proof suitable for academic publication can easily take multiple years to formalize to the degree it can be verified by computer. Yes of course a large part depends on formalizing prior authors' work, but both are hard -- the prior stuff and your new stuff. Your assertion that there's "nothing difficult" is contradicted by all the mathematicians I know. |
|
|
|
|
|
| |
| ▲ | pxc 2 days ago | parent | prev | next [-] | | For one, some geometric proofs by construction can literally involve pictures rather than statements, right? | | |
| ▲ | DoctorOetker 2 days ago | parent [-] | | Sure the history of mathematics used many alternative conceptions of "proof". The problem is that such constructions were later found to be full of hidden assumptions. Like working in a plane vs on a spherical surface etc. The advantage of systems like MetaMath are: 1. prover and verifier are essentially separate code bases, indeed the MM prover is essentially absent, its up to humans or other pieces of software to generate proofs. The database just contains explicit axioms, definitions, theorems claims, with proofs for each theorem. The verifier is a minimalistic routine with a minimum amount of lines of code (basically substitution maps, with strict conditions). The proof is a concrete object, a finite list of steps. 2. None of the axioms are hardcoded or optimized, like they tend to be in proof systems where proof search and verification are intermixed, forcing axioms upon the user. |
| |
| ▲ | variaga 2 days ago | parent | prev [-] | | >Do you just mean that we must assume something to get the ball rolling They're called "axioms" |
| |
| ▲ | RossBencina 2 days ago | parent | prev [-] | | > mathematics isn't just a giant machine of deductive statements I think the subject at question here is mathematical truth, not "mathematics" whatever that means. |
| |
| ▲ | DoctorOetker 2 days ago | parent | prev | next [-] | | >You say that like it’s even remotely feasible at the frontier of mathematics and not a monumental group effort to turn even established proofs into such. Is it really known to be the frontier as long as its not verified? I would call the act of rigorous verification the acknowledgement of a frontier shift. Consider your favorite dead-end in science, perhaps alchemy, the search for alcahest, the search for the philosophers stone, etc. I think nobody today would pretend these ideas were at the frontier, because today it is collectively identified as pseudoscience, which failed to replicate / verify. If I were the first to place a flag on some mountain, that claim may or may not be true in the eyes of others, but time will tell and others replicating the feat will be able to confirm observation of my flag. As long as no one can verify my claims they are rightfully contentious, and as more and more people are able to verify or invalidate my claims it becomes clear if I did or did not move the frontier. | |
| ▲ | DoctorOetker 2 days ago | parent | prev [-] | | One doesn't need to be an expert in machine readable mathematics, to understand how to formalize it to a machine readable form. If one takes the time to read the free book accompanying the metamath software, and re implements it in about a weekend time, you learn to understand how it works internally. Then playing around a little with mmj2 or so you quickly learn how to formalize a proof you understand. If you understand your own proof its easy to formalize it. One doesn't need to be "an expert in machine readable mathematics". | | |
| ▲ | amanaplanacanal 2 days ago | parent | next [-] | | Do you have the weekend free? Perhaps you can take this new proof and show us how it is done. | | |
| ▲ | DoctorOetker 3 hours ago | parent [-] | | If one is given an incomplete proof (i.e. where not each step is justified in terms of theorems completely justified before it) there is an amount of bruteforce entropy involved for guessing which intermediate steps weren't jotted down. Of course it takes 20x or more effort if the prover refused to write down certain steps. It even occurs that when pointed out, it takes the original "prover" a lot of time to find a proof for a gap, hence it wasn't originally proven. If I find my own proofs, or if the proof of someone else is clearly written, formalization is not hard at all. Let us assume for the sake of this discussion that Wiles' latest proof for FLT is in fact complete, while his earlier proof wasn't. It took Wiles and his helper more than a weekend to close the gap. Imagine no one had challenged the proof or pointed out this gap. Anyone tasked with formalizing it would face the challenge of trying to figure out which result (incorrectly presumed to be already known) was used in a certain step. The formalizer is in fact finishing an unfinished proof. After succeeding in closing this gap, who else was willing to point at the next gap? There is always some sense of prestige lost when pointing at a "gap" and then observing the original prover(s) close that gap, in a sense they saw how to prove it while the challenger did not. This dynamic is unhealthy. To claim a proof we should expect a complete proof, the burden of proof should lay on the proving claimant not on the verifier. |
| |
| ▲ | 2 days ago | parent | prev [-] | | [deleted] |
|
|
