I made an 800 in my math SAT.
I have been a programmer for 40 years.
I have been researching these subjects for 38 years.
I can prove my points easily.
There is a lot of BS in academia.
There is The Big Lie of Academic Computer Science

"Mathematics and Computer Science Have Been Automated"

Total BS.

1. Program Synthesis:

Input: Spec [optional: and Programming Language]
Output: Computer Program

Wikipedia is popular, well respected and has a massive amount of information on any technical subject. Look up Godel, Turing, Recursion Theory etc. and there are pages of really good well-arranged material. There are a great source of the state-of-the-art.

Look up wiki program synthesis.
There is ONE "example".
Read it.
It is stupid nonsense.
1. It starts by requiring you to input the program you want to create, in "rules". Really. It is insane. Program in Line 58: p ? s : t
2. You go through some gyrations with no explanation as to how you determine what to do.
3. It admits it is not automated.
4. The output is the program from the "rule" you entered in (1).
5. The "program" is x<y ? y : x
Input p ? s : t and output x<y ? y : x.
It only produces the program that you input.
That is the ONLY EXAMPLE. They list dozens of references. That is all they can find.

WHY? Explain this, please?
Answer: None of the professors or researchers have figured it out.

I have pointed this out a dozen times. All I receive is nonsense. He says to read other references with other examples. So why not list a better example? I know those references. They are the same nonsense. I am asking about the example given. THAT we can talk about. It is in front of us.

Look up Program Synthesis on the internet or in You Tube videos. You get he same result. NO EXAMPLES. Nobody has ever generated a single program. TELL US THE PROCEDURE FOR GENERATING PRORAMS. THERE IS NONE. They claim an occasional example but it is the same nonsense. NO PROCEDURE IS GIVEN. Just a mass of formulas and at the end there is a program (at best.)

2. Automatic Theorem Proving.

They have never produced any new theorem.
They give one example in a paper with pages of formulas and claims and NO PROCEDURE FOR PRODUCING IT.

A theorem-generator does nor produce ONE (existing) theorem. It produces an infinite number of theorems. Turn it on and they come one.

Go through the articles of ANY academic journal. 100% of them are from colleges and a few huge company research departments. It is the Old Boy's Club. Only the true believers (BS artists) are allowed.

Just like the American Republican political party. Their Big Lie is that Donald Trump won the 2020 election and Joe Biden stole it. Right now they are being prosecuted for a HUGE scheme to install him as president using fake scenarios: Declare martial law. Force the state legislatures to send Republican liars to the Electoral College. 60 lawsuits claiming fraud in key states - ALL thrown out.

Come January 2022 weeks of hearings begin. THEY will go to jail.

When will the hearings on the liar professors begin?

HA!

C-B

Charlie-Boo <shymathguy@gmail.com> writes:

> I made an 800 in my math SAT.

I don't know what that means. I think it's a USA thing.

> I have been a programmer for 40 years.

That's a rather narrow career. I suppose you must enjoy it.

> I have been researching these subjects for 38 years.

And have you published anything on these subjects? Good research
usually ends up with something worth saying.

> I can prove my points easily.

That's good.

> There is a lot of BS in academia.

Yes, there is a lot of BS everywhere, but comp.theory must be close to
being the top place for BS recently. Would it not be better to write
somewhere else? By writing here, you risk having what you write taken
as BS even if it is not.

> There is The Big Lie of Academic Computer Science
>
> "Mathematics and Computer Science Have Been Automated"

That appears to be a quote. Who said it? If it's not a quote, why
would you say it?

> Total BS.

Agreed. But is this a strawman. Who are you quoting?

--
Ben.

On 12/26/2021 10:03 AM, Charlie-Boo wrote:
> I made an 800 in my math SAT.
> I have been a programmer for 40 years.
> I have been researching these subjects for 38 years.
> I can prove my points easily.
> There is a lot of BS in academia.
> There is The Big Lie of Academic Computer Science
>
> "Mathematics and Computer Science Have Been Automated"
>
> Total BS.
>
> 1. Program Synthesis:
>
> Input: Spec [optional: and Programming Language]
> Output: Computer Program
>
> Wikipedia is popular, well respected and has a massive amount of information on any technical subject. Look up Godel, Turing, Recursion Theory etc. and there are pages of really good well-arranged material. There are a great source of the state-of-the-art.

In general Wikipedia is not academia. Even you or I might be able to
contribute. You will notice a mess of inconsistent notations among all
those articles. A nightmare.

> Look up wiki program synthesis.
> There is ONE "example".
> Read it.
> It is stupid nonsense.
> 1. It starts by requiring you to input the program you want to create, in "rules". Really. It is insane. Program in Line 58: p ? s : t
> 2. You go through some gyrations with no explanation as to how you determine what to do.
> 3. It admits it is not automated.
> 4. The output is the program from the "rule" you entered in (1).
> 5. The "program" is x<y ? y : x
> Input p ? s : t and output x<y ? y : x.
> It only produces the program that you input.
> That is the ONLY EXAMPLE. They list dozens of references. That is all they can find.

There have been many attempts to do program synthesis and that is quite
different than automating systems requirements and specification. Surely
you know that. Do you?

> WHY? Explain this, please?
> Answer: None of the professors or researchers have figured it out.
>
> I have pointed this out a dozen times. All I receive is nonsense. He says to read other references with other examples. So why not list a better example? I know those references. They are the same nonsense. I am asking about the example given. THAT we can talk about. It is in front of us.
>
> Look up Program Synthesis on the internet or in You Tube videos. You get he same result. NO EXAMPLES. Nobody has ever generated a single program. TELL US THE PROCEDURE FOR GENERATING PRORAMS. THERE IS NONE. They claim an occasional example but it is the same nonsense. NO PROCEDURE IS GIVEN. Just a mass of formulas and at the end there is a program (at best.)

> 2. Automatic Theorem Proving.
>
> They have never produced any new theorem.
> They give one example in a paper with pages of formulas and claims and NO PROCEDURE FOR PRODUCING IT.

For this one, I suggest that you look up Doug Lenat's dissertation done
at Stanford. It was called "The Assistant Mathematician". It didn't
prove theorems; it just generated interesting conjectures. No one at the
Stanford Math Department knew anything about one of them. Paul Erdos
happened to visit and was able to provide an obscure reference for it,
in an old Indian math journal. The article was by Ramanujen (however
that is spelled). So yes, there is some real results here.

On a different slant: Computer assisted theorem proving was used in
several security system/model verification as part of secure
trust-at-a-level certification for OS and network software. Some cases
were proved viable and others were shown to fail, i.e., showing failure
meant showing that theorems supporting necessary conditions were false,
hence, the system could not meet its objectives. By the way, one of
these proofs could be longer than the longest Wiki article (and that was
why the proofs need computer assistance).

> A theorem-generator does nor produce ONE (existing) theorem. It produces an infinite number of theorems. Turn it on and they come one.
>
> Go through the articles of ANY academic journal. 100% of them are from colleges and a few huge company research departments. It is the Old Boy's Club. Only the true believers (BS artists) are allowed.
>
> Just like the American Republican political party. Their Big Lie is that Donald Trump won the 2020 election and Joe Biden stole it. Right now they are being prosecuted for a HUGE scheme to install him as president using fake scenarios: Declare martial law. Force the state legislatures to send Republican liars to the Electoral College. 60 lawsuits claiming fraud in key states - ALL thrown out.
>
> Come January 2022 weeks of hearings begin. THEY will go to jail.
>
> When will the hearings on the liar professors begin?

You want to criticize Academia (notice the capitol A) for bull shit.
Well look at you: a single article 1) bragging about your SAT score, 2)
criticizing program synthesis efforts and no citations to the actual
literature, only to baby stuff, 3) criticism of automated theorem
proving that starts by criticizing theorem formulation instead, once
again without any research other than comic books, and 4) end up talking
about Trump.

I think this is an incoherent thread and if you are really interested in
any of these topics that you need to stop challenging others to do your
research for you and dig into really literature. Wikipedia is for
virtually everyone to get a taste. If your looking for deeper knowledge,
you'll need to earn it.
--
Jeff Barnett

On Sunday, December 26, 2021 at 12:31:49 PM UTC-5, Ben Bacarisse wrote:
> Charlie-Boo <shyma...@gmail.com> writes:

>> I made an 800 in my math SAT.
> I don't know what that means. I think it's a USA thing.

Perfect score on the test given by virtually every college to test your ability to master their material. A perfect score is rare.

>> I have been a programmer for 40 years.
> That's a rather narrow career.

What's the point? How's that? Virtually every programmer I know stays with it for life or moves into management (for obvious reasons.)

>> I have been researching these subjects for 38 years.
>And have you published anything on these subjects? Good research usually ends up with something worth saying.

"Handbook of Efficiency Techniques" - 184 pages. Very popular among M programmers. If you must know: I was once surrounded by a dozen people at a computer conference.

About 10 articles in trade publications. On programming, programming language design and design of implementation of programming languages.

Number of articles accepted by academic journals: 0

Is this Ad Hominem reasoning?

On the brighter side - not to brag, but - a few professors read my posts on FOM (Foundations of Mathematics - refereed by about 6 professors) and apparently elsewhere (Martin Davis, Gio Wiederhold and at least one other whom I forget), contacted me with questions, asked me to create a class on it to be given there, asked me to join a contingency of computer scientists representing the United States in a cultural exchange with China, etc. For better or worse, I turned them down for the most part. I do NOT want to join the crooks before exposing them - if ever. I USED to try and now I realize that was a mistake.

>> There is a lot of BS in academia.
> Yes, there is a lot of BS everywhere.

In academic Mathematics research and publishing? Name one.

> comp.theory must be close to being the top place for BS recently.
> Would it not be better to write somewhere else?

They are not mutually exclusive. I rarely write here. It’s full of nonsense. Just for a lark I decided to spell it all out. Your words notwithstanding, many professors participate in this forum. One intent is to see their defenses. It is always interesting to see someone try to defend a blatant lie. It's fun to prove a liar to be a liar. Far too often they get away with it. It's good practice. I've written to a couple. One wrote and all he did was lie.

> By writing here, you risk having what you write taken as BS even if it is not.

I think you miss the point. The Academic Big Lie is everywhere. I sent a copy of an ARXIV paper I wrote on it to a Microsoft Research big-wig and he flipped out. If he thought I was a crank I assume he would have ignored it. He actually asked if he could call me, I said ok, and all he said on the phone was to tell me not to publish it because it was well-known in the 1990's and has been replaced by better methods. Unfortunately I just listened instead of asking for references.

>> There is The Big Lie of Academic Computer Science
>> "Mathematics and Computer Science Have Been Automated"
>That appears to be a quote. Who said it? If it's not a quote, why would you say it?

It is MY quote.

>> Total BS.
>Agreed. But is this a strawman. Who are you quoting?

Me.

What are you agreeing to, exactly?
What am I misrepresenting and how?

C-B

On Sunday, December 26, 2021 at 12:31:49 PM UTC-5, Ben Bacarisse wrote:
> Charlie-Boo <shyma...@gmail.com> writes:
>
> > I made an 800 in my math SAT.
> I don't know what that means. I think it's a USA thing.
> > I have been a programmer for 40 years.
> That's a rather narrow career. I suppose you must enjoy it.
> > I have been researching these subjects for 38 years.
> And have you published anything on these subjects? Good research
> usually ends up with something worth saying.

Yes, but publication in academic journals might involve working with right-wing extremists who discriminate against disabled/minority groups and might even lie about the accuracy of research efforts, just like comp.theory posters. How do you feel about recommending that to people on the internet without qualification? It is very legitimate to be a math/CS researcher who rejects dishonesty, fraud, laziness, discrimination, and, by extension, modern academic publishing. Such researchers can be quietly very effective in at least one sense.

-Philip

> > I can prove my points easily.
> That's good.
> > There is a lot of BS in academia.
> Yes, there is a lot of BS everywhere, but comp.theory must be close to
> being the top place for BS recently. Would it not be better to write
> somewhere else? By writing here, you risk having what you write taken
> as BS even if it is not.
> > There is The Big Lie of Academic Computer Science
> >
> > "Mathematics and Computer Science Have Been Automated"
> That appears to be a quote. Who said it? If it's not a quote, why
> would you say it?
>
> > Total BS.
>
> Agreed. But is this a strawman. Who are you quoting?
>
> --
> Ben.

Charlie-Boo <shymathguy@gmail.com> writes:

> On Sunday, December 26, 2021 at 12:31:49 PM UTC-5, Ben Bacarisse wrote:
>> Charlie-Boo <shyma...@gmail.com> writes:
>
>>> I made an 800 in my math SAT.
>> I don't know what that means. I think it's a USA thing.
>
> Perfect score on the test given by virtually every college to test
> your ability to master their material. A perfect score is rare.
>
>>> I have been a programmer for 40 years.
>> That's a rather narrow career.
>
> What's the point? How's that? Virtually every programmer I know
> stays with it for life or moves into management (for obvious reasons.)

It seemed a narrow focus for someone posting about formal methods, but
that might be my misinterpreting "programmer". Maybe you have practical
experience with formal methods as part of being programmer.

>>> I have been researching these subjects for 38 years.
>>And have you published anything on these subjects? Good research
>>usually ends up with something worth saying.
>
> "Handbook of Efficiency Techniques" - 184 pages. Very popular among M
> programmers. If you must know: I was once surrounded by a dozen
> people at a computer conference.

Is that "The MUMPS Handbook of Efficiency Techniques: 125 Ways to Make
Your MUMPS Applications Run Faster"? I could not find anything else
with a closely matching title.

> About 10 articles in trade publications. On programming, programming
> language design and design of implementation of programming languages.
>
> Number of articles accepted by academic journals: 0
>
> Is this Ad Hominem reasoning?

No, it was a desire to find out whether I could read your work in the
field without struggling with your posting style. I find your posts
unclear and quite hard to read, but a published paper will have gone
through an editorial process that will result in a clearer presentation.

But the publications you cite do not appear to be about the topic you
are posting on.

> On the brighter side - not to brag, but - a few professors read my
> posts on FOM (Foundations of Mathematics - refereed by about 6
> professors) and apparently elsewhere (Martin Davis, Gio Wiederhold and
> at least one other whom I forget), contacted me with questions, asked
> me to create a class on it to be given there, asked me to join a
> contingency of computer scientists representing the United States in a
> cultural exchange with China, etc. For better or worse, I turned them
> down for the most part. I do NOT want to join the crooks before
> exposing them - if ever. I USED to try and now I realize that was a
> mistake.

You are calling Martin Davis a crook? Interesting.

>>> There is a lot of BS in academia.
>> Yes, there is a lot of BS everywhere.
>
> In academic Mathematics research and publishing? Name one.

Famously, a resident crank in comp.math got a paper published but the
journal went under shortly afterwards. Some people saw a connection!

>> comp.theory must be close to being the top place for BS recently.
>> Would it not be better to write somewhere else?
>
> They are not mutually exclusive. I rarely write here. It’s full of
> nonsense. Just for a lark I decided to spell it all out. Your words
> notwithstanding, many professors participate in this forum. One
> intent is to see their defenses. It is always interesting to see
> someone try to defend a blatant lie. It's fun to prove a liar to be a
> liar. Far too often they get away with it. It's good practice. I've
> written to a couple. One wrote and all he did was lie.
>
>> By writing here, you risk having what you write taken as BS even if it is not.
>
> I think you miss the point. The Academic Big Lie is everywhere. I
> sent a copy of an ARXIV paper I wrote on it to a Microsoft Research
> big-wig and he flipped out. If he thought I was a crank I assume he
> would have ignored it. He actually asked if he could call me, I said
> ok, and all he said on the phone was to tell me not to publish it
> because it was well-known in the 1990's and has been replaced by
> better methods. Unfortunately I just listened instead of asking for
> references.

What's the paper? I'd like to read it.

>>> There is The Big Lie of Academic Computer Science
>>> "Mathematics and Computer Science Have Been Automated"
>>That appears to be a quote. Who said it? If it's not a quote, why
>>would you say it?
>
> It is MY quote.

Ah. I thought it might be. Why do you want to argue against your own
quote? That's the very definition of a straw man.

--
Ben.

On Sunday, December 26, 2021 at 1:42:16 PM UTC-5, Jeff Barnett wrote:
> On 12/26/2021 10:03 AM, Charlie-Boo wrote:

>> Wikipedia is popular, well respected and has a massive amount of information on any technical subject.
>> They are a great source of the state-of-the-art.

> In general Wikipedia is not academia.

I'm not saying it is. I'm using it as a reference that (1) we can all access easily, (2) has a huge database of information of technical subjects, (3) is updated constantly. Unbelievably, virtually every page has had an update within the past few days or so.

That makes them a good starting point for the state-of-the-art. Pick a random technical topic and then let's see if they represent the state-of-the art.

>> Look up wiki program synthesis.
.. . .
>> It only produces the program that you input.
>> That is the ONLY EXAMPLE. They list dozens of references. That is all they can find.

> There have been many attempts to do program synthesis and that is quite different than automating systems requirements and specification. Surely
you know that. Do you?

What are you talking about? Who said anything about "automating systems requirements and specification"? How could that be possible? The specification is the input that the user creates. How can you have a system tell you what you want? There are many systems to represent specifications. That is not the point of this thread. It is SPECIFICATION => PROGRAM.

>> 2. Automatic Theorem Proving.
>> They have never produced any new theorem.
>> They give one example, pages of formulas and NO PROCEDURE FOR PRODUCING IT.

> Doug Lenat's dissertation at Stanford "The Assistant Mathematician" didn't prove theorems; it just generated interesting conjectures. No one at the Stanford Math Department knew anything about one of them. So yes, there is some real results here.

Conjectures can be generated by looking for patterns and the conjecture is that it always occurs. Start with any positive integer and repeatedly apply function IF even(x) x/2 ELSE x*3+1. It reaches the 4-2-1 loop for every number ever tested. Does it always?

It is easy to generate random functions and run this test. This one has been an unsolved problem for 84 years. It's not that hard to generate conjectures. It can be very difficult to prove them. Automated Theorem Proving is about proving them. Generating conjectures per se does nothing to help Automated Theorem Proving. How does that help?

> Computer assisted theorem proving was used in several security system/model verifications for OS and network software.

"Computer assisted theorem proving" requires the person to enter in the steps and it verifies the logic of each step. Theorem Proving is the problem of determining the steps. Many mathematicians can verify the logic of each step in the proof of Fermat's Last Theorem but could they have produced that proof?

> You want to criticize Academia (notice the capitol A) for bull shit. Well look at you:
> a single article

How do we prove something has not been solved? In journal articles offering a solution they review the literature, especially the state-of-the-art papers. I chose Wikipedia as an easily accessed state-of-the-art. What should I do?

> bragging about your SAT score

Attempting to head off those who just call people stupid.

> criticizing program synthesis efforts and no citations to the actual literature

Program Synthesis ~ Sumit Gulwani, Oleksandr Polozov, Rishabh Singh

The entire book is about hand-written general programs for specific problems e.g. writing expressions for Excel spreadsheets.

> criticism of automated theorem proving that starts by criticizing theorem formulation instead

What are you talking about?

> I think this is an incoherent thread and if you are really interested in any of these topics that you need to stop challenging others to do your research for you and dig into really literature.

It's coherent enough for you to respond. I said I've been studying it for years. I have every book I could find and at least 100 articles on it. Actually, I once paid 3 people to find 100 references each: books, websites and articles as pdfs. Unfortunately I can't attach a PDF of some of my Amazon purchases of used international conference proceedings bought at a huge discount. https://smile.amazon.com/gp/product/3540630457/ref=ppx_yo_dt_b_asin_title_o03_s00?ie=UTF8&psc=1

But this isn't even the purpose of this thread. Read the subject.
--
Jeff Barnett

On Sunday, December 26, 2021 at 3:15:08 PM UTC-5, B.H. wrote:
> On Sunday, December 26, 2021 at 12:31:49 PM UTC-5, Ben Bacarisse wrote:
> > Charlie-Boo <shyma...@gmail.com> writes:
> >
> > > I made an 800 in my math SAT.
> > I don't know what that means. I think it's a USA thing.
> > > I have been a programmer for 40 years.
> > That's a rather narrow career. I suppose you must enjoy it.
> > > I have been researching these subjects for 38 years.
> > And have you published anything on these subjects? Good research
> > usually ends up with something worth saying.
> Yes, but publication in academic journals might involve working with right-wing extremists who discriminate against disabled/minority groups and might even lie about the accuracy of research efforts, just like comp.theory posters. How do you feel about recommending that to people on the internet without qualification? It is very legitimate to be a math/CS researcher who rejects dishonesty, fraud, laziness, discrimination, and, by extension, modern academic publishing. Such researchers can be quietly very effective in at least one sense.

I think you've lost me. It sounds like you’re replying to Ben.

In any case: There are honest researchers. The most honest Program Synthesis researchers were probably Zohar Manna and Richard Waldinger. (I actually spent 2 afternoons with them when I was on the west coast many years ago. Richard showed me his display of family photos and Zohar was very jovial. When I told him a paradox of mine, he took me to a guy who would be more interested. Unfortunately, he was the opposite of Zohar. Then some barefooted guy walked in. When I told Zohar I found some errors in his Mathematical Theory of Computation, he laughed and said, "Oh, there are plenty of them." and held up his copy with the cover coming off. Mine were only typos.)

There are honest researchers but they don't write about a successful Program Synthesis system. ZM/RW wrote honest efforts to use proof to create tiny programs of no value e.g. division by repeated subtraction. Around the 1990's they wrote what seems to be their last Program Synthesis paper, and said they could not succeed because theorem-provers weren't powerful enough. My thought there is that a prototype could be developed that had tables for the needed theorem-proving.

But writing honest papers for BS journals must be nerve-racking.

How can honest researchers be effective?

On Sunday, December 26, 2021 at 5:42:39 PM UTC-5, Charlie-Boo wrote:
> On Sunday, December 26, 2021 at 3:15:08 PM UTC-5, B.H. wrote:
> > On Sunday, December 26, 2021 at 12:31:49 PM UTC-5, Ben Bacarisse wrote:
> > > Charlie-Boo <shyma...@gmail.com> writes:
> > >
> > > > I made an 800 in my math SAT.
> > > I don't know what that means. I think it's a USA thing.
> > > > I have been a programmer for 40 years.
> > > That's a rather narrow career. I suppose you must enjoy it.
> > > > I have been researching these subjects for 38 years.
> > > And have you published anything on these subjects? Good research
> > > usually ends up with something worth saying.
> > Yes, but publication in academic journals might involve working with right-wing extremists who discriminate against disabled/minority groups and might even lie about the accuracy of research efforts, just like comp.theory posters. How do you feel about recommending that to people on the internet without qualification? It is very legitimate to be a math/CS researcher who rejects dishonesty, fraud, laziness, discrimination, and, by extension, modern academic publishing. Such researchers can be quietly very effective in at least one sense.
> I think you've lost me. It sounds like you’re replying to Ben.
>

Yes, I was writing to Ben Bacarisse mainly. I don't think I said I didn't want to respond any more...the "Dear Sister" effect wore off and I don't remember everything I write anyway.

> In any case: There are honest researchers. The most honest Program Synthesis researchers were probably Zohar Manna and Richard Waldinger. (I actually spent 2 afternoons with them when I was on the west coast many years ago. Richard showed me his display of family photos and Zohar was very jovial. When I told him a paradox of mine, he took me to a guy who would be more interested. Unfortunately, he was the opposite of Zohar. Then some barefooted guy walked in. When I told Zohar I found some errors in his Mathematical Theory of Computation, he laughed and said, "Oh, there are plenty of them." and held up his copy with the cover coming off. Mine were only typos.)
>

I agree that there are good honest researchers. Will I name one other than me? Well, would I get attacked and watch "The Return of Dear Sister" in at least one way if I did?

> There are honest researchers but they don't write about a successful Program Synthesis system. ZM/RW wrote honest efforts to use proof to create tiny programs of no value e.g. division by repeated subtraction. Around the 1990's they wrote what seems to be their last Program Synthesis paper, and said they could not succeed because theorem-provers weren't powerful enough. My thought there is that a prototype could be developed that had tables for the needed theorem-proving.
>

I think it is healthier and better to prove theorems by hand. Thinking about topology is healthy; proving your own theorems is healthy. You wouldn't want a computer to read books for you or negotiate on your behalf, either.

> But writing honest papers for BS journals must be nerve-racking.
>
> How can honest researchers be effective?

My advice is: You should make sure that you know why you are doing research. Is the market/organization that you want to supply to--whether that's academic journals in Uzbekistan or somewhere, a firm in the tech startup world, intellectual property markets in the US, or your own personal "mathematical art science" stash that you want to augment--available to you? Don't settle for a market you don't like if you don't have to, and be prepared to fight/compete to access your chosen market if you must.

-Philip

On 12/26/2021 3:08 PM, Charlie-Boo wrote:
> On Sunday, December 26, 2021 at 1:42:16 PM UTC-5, Jeff Barnett wrote:
>> On 12/26/2021 10:03 AM, Charlie-Boo wrote:
>
>>> Wikipedia is popular, well respected and has a massive amount of information on any technical subject.
>>> They are a great source of the state-of-the-art.
>
>> In general Wikipedia is not academia.
>
> I'm not saying it is. I'm using it as a reference that (1) we can all access easily, (2) has a huge database of information of technical subjects, (3) is updated constantly. Unbelievably, virtually every page has had an update within the past few days or so.
>
> That makes them a good starting point for the state-of-the-art. Pick a random technical topic and then let's see if they represent the state-of-the art.
>
>>> Look up wiki program synthesis.
> . . .
>>> It only produces the program that you input.
>>> That is the ONLY EXAMPLE. They list dozens of references. That is all they can find.
>
>> There have been many attempts to do program synthesis and that is quite different than automating systems requirements and specification. Surely
> you know that. Do you?
>
> What are you talking about? Who said anything about "automating systems requirements and specification"? How could that be possible? The specification is the input that the user creates. How can you have a system tell you what you want? There are many systems to represent specifications. That is not the point of this thread. It is SPECIFICATION => PROGRAM.
>
>>> 2. Automatic Theorem Proving.
>>> They have never produced any new theorem.
>>> They give one example, pages of formulas and NO PROCEDURE FOR PRODUCING IT.
>
>> Doug Lenat's dissertation at Stanford "The Assistant Mathematician" didn't prove theorems; it just generated interesting conjectures. No one at the Stanford Math Department knew anything about one of them. So yes, there is some real results here.
>
> Conjectures can be generated by looking for patterns and the conjecture is that it always occurs. Start with any positive integer and repeatedly apply function IF even(x) x/2 ELSE x*3+1. It reaches the 4-2-1 loop for every number ever tested. Does it always?

Once again, I give you a solid lead but your not interested. The whole
point of Lenat's work was to decide what would be interesting an might
be true. In other words, to pick among millions of possibilities those
that would be interesting. In art, that talent is more important than
knowing brush techniques, in math and science, that talent separates low
accomplishment also runs from Nobel Laureates. Your criticizing
something suggested to you that you don't want to read and don't care
what it is actually about. I'll assume that is whining.

> It is easy to generate random functions and run this test. This one has been an unsolved problem for 84 years. It's not that hard to generate conjectures. It can be very difficult to prove them. Automated Theorem Proving is about proving them. Generating conjectures per se does nothing to help Automated Theorem Proving. How does that help?
>
>> Computer assisted theorem proving was used in several security system/model verifications for OS and network software.
>
> "Computer assisted theorem proving" requires the person to enter in the steps and it verifies the logic of each step. Theorem Proving is the problem of determining the steps. Many mathematicians can verify the logic of each step in the proof of Fermat's Last Theorem but could they have produced that proof?

Once again, you don't have the foggiest idea what you are talking about.
Since you wouldn't read any real publications suggested to you, I want
make suggestions.

>> You want to criticize Academia (notice the capitol A) for bull shit. Well look at you:
>> a single article
>
> How do we prove something has not been solved? In journal articles offering a solution they review the literature, especially the state-of-the-art papers. I chose Wikipedia as an easily accessed state-of-the-art. What should I do?

Apply your brain to something with more substance. The reason Wikipedia
changes so much is a lot of folks are trying to make articles reference
their stuff instead of someone else's. The articles are reviewed but
often not by academics who have devoted their lives to narrow areas and
specialized knowledge. They have better things to do.

>> bragging about your SAT score
>
> Attempting to head off those who just call people stupid.
>
>> criticizing program synthesis efforts and no citations to the actual literature
>
> Program Synthesis ~ Sumit Gulwani, Oleksandr Polozov, Rishabh Singh
>
> The entire book is about hand-written general programs for specific problems e.g. writing expressions for Excel spreadsheets.
>
>> criticism of automated theorem proving that starts by criticizing theorem formulation instead
>
> What are you talking about?
>
>> I think this is an incoherent thread and if you are really interested in any of these topics that you need to stop challenging others to do your research for you and dig into really literature.
>
> It's coherent enough for you to respond. I said I've been studying it for years. I have every book I could find and at least 100 articles on it. Actually, I once paid 3 people to find 100 references each: books, websites and articles as pdfs. Unfortunately I can't attach a PDF of some of my Amazon purchases of used international conference proceedings bought at a huge discount. https://smile.amazon.com/gp/product/3540630457/ref=ppx_yo_dt_b_asin_title_o03_s00?ie=UTF8&psc=1
>
> But this isn't even the purpose of this thread. Read the subject.

It's hard to take anyone seriously who spends so much time talking about
why scientist and research are not honest. Then, wait it!!!! Criticizes
Trump, the king detractor from the very same people. Your ridiculous.
You and Trump could be best buddies. Some advice: If you are unfortunate
enough to get COVID, skip the Ivermectin and put your faith in those who
have some training in the area. I know you are very much like Trump but
don't trust his medical advise.

And by the way, about your 800 SAT score (math only I presume). I had a
high school math class where 23 out 0f 25 (if I remember correctly) got
800 in math. Most also got 800 in the language skills portion. One who
aced both ended up in England where he coached a (National?) women's
basketball team for years and wrote a few mystery novels. It's no big
deal really. I'm guessing thousands, if not 10's of thousands, score 800
on a SAT every year.
--
Jeff Barnett

> On Sunday, December 26, 2021 at 12:31:49 PM UTC-5, Ben Bacarisse wrote:
>> Charlie-Boo <shyma...@gmail.com> writes:

>> About 10 articles in trade publications. On programming, programming
>> language design and design of implementation of programming languages.

>> Number of articles accepted by academic journals: 0

>> Is this Ad Hominem reasoning?

>But the publications you cite do not appear to be about the topic you are posting on.

Note the number of articles accepted by academic journals. Those were on these topics.

But the point isn't my own successes. It is solely the lies around the claims of success by academia.
Isn't talking about the person who makes a claim the definition of Ad Hominem reasoning?

> On the brighter side - not to brag, but - a few professors read my
> posts on FOM (Foundations of Mathematics - refereed by about 6
> professors) and apparently elsewhere (Martin Davis, Gio Wiederhold and
> at least one other whom I forget), contacted me with questions, asked
> me to create a class on it to be given there, asked me to join a
> contingency of computer scientists representing the United States in a
> cultural exchange with China, etc. For better or worse, I turned them
> down for the most part. I do NOT want to join the crooks before
> exposing them - if ever. I USED to try and now I realize that was a
> mistake.

You are calling Martin Davis a crook? Interesting.

No, he was the lone honest one of that bunch, as you can see from his behavior. He even quoted me and defended me against the crooks. (I never could understand why he let them be there. I guess he was super busy.) When I proved 3 incompleteness theorems of Godel, Rosser and Smullyan in 18 words using Recursion Theory, they flipped out and said really stupid things like "You left out the definition of truth." Sometimes he would prove them wrong, which really shut them up!

>>>> There is a lot of BS in academia.
>>> Yes, there is a lot of BS everywhere.
>> In academic Mathematics research and publishing? Name one.
>Famously, a resident crank in comp.math got a paper published but the
journal went under shortly afterwards. Some people saw a connection!

Thanks for proving my point.

>>>> There is The Big Lie of Academic Computer Science
>>>> "Mathematics and Computer Science Have Been Automated"
>>>That appears to be a quote. Who said it? If it's not a quote, why
>>>would you say it?

>> It is MY quote.

>Ah. I thought it might be. Why do you want to argue against your own
quote? That's the very definition of a straw man.

I am quoting the Big Lie. Papers that claim to have solved Program Synthesis and Automated Theorem-Proving are making this claim. It is a lie. The papers are BS.

I'll say it nice and simple:

1. Academic computer science claims that they have developed systems to automate computer science.
2. This includes software to write computer programs and to prove theorems of mathematics.
3. So they are saying "Mathematics and Computer Science Have Been Automated".
4. I showed that the state-of-the-art for Program Synthesis on Wikipedia is stupid nonsense.
5. I showed the very structure and contents of the automation of theorem-proving papers belies their claims.

6. Nonsense on Automated Theorem-Proving:
A Mechanical Proof of the Unsolvability of the Halting Problem ~ Robert S. Boyer, J. Strother Moore
This is an article about a theorem-prover that proves only one theorem. That alone makes no sense. Even worse, how it works and even the proof itself are not given.

7. Nonsense on Program Synthesis:
Constructive mathematics and computer programming
P. Martin-Lof

His thesis: The specification is (aA)P(A) => (eB)Q(A,B). The input is A and the output is B. P() checks it is legal input and Q(,) is the relationship between the input and output. Proof of that wff produces the program. He never gave any examples of programs produced. How can he? His procedure makes no reference to the programming language in which the program must be written. The whole process depends on the functions supplied by the programming language and the syntax used to invoke them.

C-B

Charlie-Boo <shymathguy@gmail.com> writes:

>> On Sunday, December 26, 2021 at 12:31:49 PM UTC-5, Ben Bacarisse wrote:
>>> Charlie-Boo <shyma...@gmail.com> writes:

The attribution lines appear to be all messed up (and most are
missing).

>> On the brighter side - not to brag, but - a few professors read my
>> posts on FOM (Foundations of Mathematics - refereed by about 6
>> professors) and apparently elsewhere (Martin Davis, Gio Wiederhold and
>> at least one other whom I forget), contacted me with questions, asked
>> me to create a class on it to be given there, asked me to join a
>> contingency of computer scientists representing the United States in a
>> cultural exchange with China, etc. For better or worse, I turned them
>> down for the most part. I do NOT want to join the crooks before
>> exposing them - if ever. I USED to try and now I realize that was a
>> mistake.
>
> You are calling Martin Davis a crook? Interesting.

Your quoting has gone wrong. I asked that. It looks like you think
/I/ said he was crook and you are querying it.

> No, he was the lone honest one of that bunch, as you can see from his
> behavior. He even quoted me and defended me against the crooks.

Get someone you trust to read though the paragraph. I can't read it any
other way. I accept you did not intend it, but that's how it reads.

>>>>> There is The Big Lie of Academic Computer Science
>>>>> "Mathematics and Computer Science Have Been Automated"
>>>>That appears to be a quote. Who said it? If it's not a quote, why
>>>>would you say it?
>
>>> It is MY quote.
>
>> Ah. I thought it might be. Why do you want to argue against your own
>> quote? That's the very definition of a straw man.
>
> I am quoting the Big Lie. Papers that claim to have solved Program
> Synthesis and Automated Theorem-Proving are making this claim.

Citation please.

--
Ben.

On Sunday, December 26, 2021 at 6:37:44 PM UTC-5, Jeff Barnett wrote:
> On 12/26/2021 3:08 PM, Charlie-Boo wrote:
> > On Sunday, December 26, 2021 at 1:42:16 PM UTC-5, Jeff Barnett wrote:
> > > On 12/26/2021 10:03 AM, Charlie-Boo wrote:

> Once again, I give you a solid lead but your not interested. The whole
> point of Lenat's work was to decide what would be interesting an might
> be true.

Right. Nothing to do with proving them. And that is Automatic Theorem Proving. A real solid lead.

> > > Computer assisted theorem proving was used in several security system/model verifications for OS and network software.
> >
> > "Computer assisted theorem proving" requires the person to enter in the steps and it verifies the logic of each step. Theorem Proving is the problem of determining the steps. Many mathematicians can verify the logic of each step in the proof of Fermat's Last Theorem but could they have produced that proof?
>
> Once again, you don't have the foggiest idea what you are talking about.

Then tell us what Computer assisted theorem proving does.

> Since you wouldn't read any real publications suggested to you, I want
> make suggestions.

Your suggestion is about generating conjectures. That has nothing to do with proving them.
And now you have run out of suggestions.

> > How do we prove something has not been solved? In journal articles offering a solution they review the literature, especially the state-of-the-art papers. I chose Wikipedia as an easily accessed state-of-the-art. What should I do?

> Apply your brain to something with more substance.

That doesn't say anything about how to prove that something has not been solved. I did it the way any paper does.
I reviewed the state-of-the-art and it is nonsense.
And elsewhere in this thread I examine two very famous papers.

> It's hard to take anyone seriously who spends so much time talking about
> why scientist and research are not honest.

No, I said very clearly it is the automation of computer science that is not honest.
If Program Synthesis is real then why are there no examples of it?
Program Synthesis by Sumit Gulwani , Oleksandr Polozov and Rishabh Singh is an extensive survey. You can find a free pdf of it on the internet.
It has no examples. It is only hand-written programs that solve problems like writing Excel spreadsheet expressions.

> Then, wait it!!!! Criticizes
> Trump, the king detractor from the very same people.

I think you miss the point. Trump's claim of having won the 2020 election are being called The Big Lie.
He offers no proof that there was anything wrong with the election.
But despite being proven false, about 30% of Americans believe him.

Program Synthesis and Automated Theorem Proven are The Big Lie of the academic world.
They offer no proof - no examples of programs or theorems being generated.
Yet they keep publishing their papers and producing YouTube videos of people with formulas but no programs or theorems being generated and no methods of generating them.

> And by the way, about your 800 SAT score (math only I presume). I had a
> high school math class where 23 out 0f 25 (if I remember correctly) got
> 800 in math. Most also got 800 in the language skills portion.

A test that is used by essentially every college/university in the United States to decide who to admit and 94% of the people make a perfect score on math.
94% tied for first place. And half tied for first place in English with a perfect score.

How can you decide who to accept with a test in which half or more of the people are tied for first place?

The same way you generate computer programs and mathematical theorems without a way to do it?

> It's no big deal really. I'm guessing thousands, if not 10's of thousands, score 800 on a SAT every year.

Doesn't the number of people who took the test have any bearing on the significance of the number of people who made a perfect score?

C-B

On Sunday, December 26, 2021 at 8:04:04 PM UTC-5, Ben Bacarisse wrote:
> Charlie-Boo <shyma...@gmail.com> writes:

> > I am quoting the Big Lie. Papers that claim to have solved Program
> > Synthesis and Automated Theorem-Proving are making this claim.
> Citation please.

See the 10th message in this thread.

Google wiki Program Synthesis.

C-B

Charlie-Boo <shymathguy@gmail.com> writes:

> On Sunday, December 26, 2021 at 8:04:04 PM UTC-5, Ben Bacarisse wrote:
>> Charlie-Boo <shyma...@gmail.com> writes:
>
>> > I am quoting the Big Lie. Papers that claim to have solved Program
>> > Synthesis and Automated Theorem-Proving are making this claim.
>> Citation please.
>
> See the 10th message in this thread.

That's not how you reference a post. How are you countqing the posts?
The 10th (in date order) that my server sees is by Jeff Barnett and he
gives nothing that looks like a citation.

> Google wiki Program Synthesis.

If you had a paper or book that claimed that mathematics and computer
science have been automated, you'd just cite it.

--
Ben.

On 12/26/2021 6:13 PM, Charlie-Boo wrote:
> On Sunday, December 26, 2021 at 6:37:44 PM UTC-5, Jeff Barnett wrote:
>> On 12/26/2021 3:08 PM, Charlie-Boo wrote:
>>> On Sunday, December 26, 2021 at 1:42:16 PM UTC-5, Jeff Barnett wrote:
>>>> On 12/26/2021 10:03 AM, Charlie-Boo wrote:
>
>> Once again, I give you a solid lead but your not interested. The whole
>> point of Lenat's work was to decide what would be interesting an might
>> be true.
>
> Right. Nothing to do with proving them. And that is Automatic Theorem Proving. A real solid lead.

I see you cut:
"2. Automatic Theorem Proving. <====== your words, dude
They have never produced any new theorem. \|/
They give one example, pages of formulas and NO PROCEDURE FOR PRODUCING IT."

I was responding to the above. Of course you forgot or just snipped it
as an act of "malicious mischief". I know you don't have any respect for
what others say, but to ignore your own words is somewhere among
trolling, dementia, and plain silliness.

>
>>>> Computer assisted theorem proving was used in several security system/model verifications for OS and network software.
>>>
>>> "Computer assisted theorem proving" requires the person to enter in the steps and it verifies the logic of each step. Theorem Proving is the problem of determining the steps. Many mathematicians can verify the logic of each step in the proof of Fermat's Last Theorem but could they have produced that proof?
>>
>> Once again, you don't have the foggiest idea what you are talking about.
>
> Then tell us what Computer assisted theorem proving does.
>
>> Since you wouldn't read any real publications suggested to you, I want
>> make suggestions.
>
> Your suggestion is about generating conjectures. That has nothing to do with proving them.
> And now you have run out of suggestions.

Look above at your "2." Deep breath and recall

>>> How do we prove something has not been solved? In journal articles offering a solution they review the literature, especially the state-of-the-art papers. I chose Wikipedia as an easily accessed state-of-the-art. What should I do?

Wikipedia is rarely state of the art anything. I hope you don't get
swallowed up in using the internet as your only source of information.

>> Apply your brain to something with more substance.
>
> That doesn't say anything about how to prove that something has not been solved. I did it the way any paper does.
> I reviewed the state-of-the-art and it is nonsense.
> And elsewhere in this thread I examine two very famous papers.
>
>> It's hard to take anyone seriously who spends so much time talking about
>> why scientist and research are not honest.
>
> No, I said very clearly it is the automation of computer science that is not honest.
> If Program Synthesis is real then why are there no examples of it?
> Program Synthesis by Sumit Gulwani , Oleksandr Polozov and Rishabh Singh is an extensive survey. You can find a free pdf of it on the internet.
> It has no examples. It is only hand-written programs that solve problems like writing Excel spreadsheet expressions.
>
>> Then, wait it!!!! Criticizes
>> Trump, the king detractor from the very same people.
>
> I think you miss the point. Trump's claim of having won the 2020 election are being called The Big Lie.
> He offers no proof that there was anything wrong with the election.
> But despite being proven false, about 30% of Americans believe him.

And if he cited Wikipedia, would you have believed him??

> Program Synthesis and Automated Theorem Proven are The Big Lie of the academic world.

Is the search for a unified field theory a Big Lie. (Did I get the
capitalization right?) One of these days someone will find a good theory
that will do good work for decades but nobody has yet.

Why your whiny attitude about people who have more education and more
knowledge than you? They've worked harder and stuck to a related set of
topics even when the going was rough. Publishing a refereed paper takes
weeks of hard work even after "you are sure you know what you want to
say". It seems you are jealous and think the world must owe you overt
recognition. It's funny, both PO and you detest Trump yet mimic his
attitude toward science and knowledge that was hard fought for. It seems
that comp.theory juxtaposes strange bedfellows.

> They offer no proof - no examples of programs or theorems being generated.
> Yet they keep publishing their papers and producing YouTube videos of people with formulas but no programs or theorems being generated and no methods of generating them.

[Before getting to the main point: YouTube, like Wikipedia has no real
controls on content. So don't put so much faith in all these Internet
freebies. They'll turn your brain to Jello, the jiggly dessert.]

They are very hard problems and some progress has been made. The
horribly hard stumbling block has always been that the computer must
either guess or be told what the requirements are. The problem is that
nobody knows them for most applications. Since most systems (OS, word
processing, games, browsers, mail clients, even compilers for many
languages) don't have detailed documentation, you can't even make the
statement "it's a bug".

>> And by the way, about your 800 SAT score (math only I presume). I had a
>> high school math class where 23 out 0f 25 (if I remember correctly) got
>> 800 in math. Most also got 800 in the language skills portion.
>
> A test that is used by essentially every college/university in the United States to decide who to admit and 94% of the people make a perfect score on math.
> 94% tied for first place. And half tied for first place in English with a perfect score.
>
> How can you decide who to accept with a test in which half or more of the people are tied for first place?
>
> The same way you generate computer programs and mathematical theorems without a way to do it?
>
>> It's no big deal really. I'm guessing thousands, if not 10's of thousands, score 800 on a SAT every year.
>
> Doesn't the number of people who took the test have any bearing on the significance of the number of people who made a perfect score?

Of course. And since every kid who might want to go to some college
takes the test. Well figure out that number do a little numerical
approximating, etc. Hey! You might look it up on the Internet. Better
would be to find out who operates the SAT program and look up their
publications or write an ask them. Oh. I forgot. You don't read
publications. So its Plan B for you.
--
Jeff Barnett

On Sunday, December 26, 2021 at 9:35:10 PM UTC-5, Ben Bacarisse wrote:
> Charlie-Boo <shyma...@gmail.com> writes:

> >> Citation please.
> >
> > See the 10th message in this thread.

MESSAGE
Charlie-Boo
Dec 26, 2021, 7:17:01 PM

> If you had a paper or book that claimed that mathematics and computer
> science have been automated, you'd just cite it.

I have referred to a few - the Program Synthesis text, at least 2 papers. These are the more famous ones.

Program Synthesis is the automation of computer programming.
Automated Theorem-Proving is the automation of theorem-proving, a fundamental part of Mathematics.

Maybe you should talk more about the subject of this thread than the author of this thread.

Google "Program Synthesis" or search for "Program Synthesis" in You Tube and you'll see plenty of sites and videos.
I have pointed out and explained some of the most blatant and extensive claims.

If you need more, I can dig up my collection of papers each of which claims to have a theorem-prover that proves exactly one (famous) theorem (I discuss one elsewhere in this thread) and a book devoted to one famous theorem.

Would it make sense that a theorem-prover would prove only one theorem? LOL

I laugh every time I think of it. How could anyone with any knowledge of theorem-proving think it makes sense?

And there are variations to these theorems as well. Some are preludes (lemmas) to each other.

On Monday, 27 December 2021 at 01:13:57 UTC, Charlie-Boo wrote:
> On Sunday, December 26, 2021 at 6:37:44 PM UTC-5, Jeff Barnett wrote:
>
> > Then, wait it!!!! Criticizes
> > Trump, the king detractor from the very same people.
> I think you miss the point. Trump's claim of having won the 2020 election are being called The Big Lie.
> He offers no proof that there was anything wrong with the election.
> But despite being proven false, about 30% of Americans believe him.
>
It takes a pretty robust belief in American exceptionalism to reject as totally implausible the
idea that Trump exceeded the tolerance of the American intelligence establishment.
>
> > And by the way, about your 800 SAT score (math only I presume). I had a
> > high school math class where 23 out 0f 25 (if I remember correctly) got
> > 800 in math. Most also got 800 in the language skills portion.
> A test that is used by essentially every college/university in the United States to decide who to admit and
> 94% of the people make a perfect score on math.
> 94% tied for first place. And half tied for first place in English with a perfect score.
>
> How can you decide who to accept with a test in which half or more of the people are tied for first place?
>
That's a problem in the UK. What we call"grade inflation" means that so many chldren have perfect
grades that it no longer guarantees entry into Oxford or Cambridge. But most people who get onto
the maths course at Oxford, even, don't end up as professional mathematicians, pushing the
boundaries of the subject. The single biggest destination for Oxford graduates is school teaching.
Learning mathematics isn't the same thing as inventing mathematics. HIgh school tests show
the university that you've got basic aptitude for numerate subjects. Whilst the tiny handful of
top future professional mathematics will be in the group with very good high school scores, the
high school tests are not designed to identify that tiny handful.
>
> The same way you generate computer programs and mathematical theorems without a way to do it?
> > It's no big deal really. I'm guessing thousands, if not 10's of thousands, score 800 on a SAT every year.
> Doesn't the number of people who took the test have any bearing on the significance of the number of people who made a perfect score?
>
Yes. Let's say you take a test in hieroglyphics, and get a perfect score. Very few people learn to read
hieroglyphics. So you are probably in the top two or three in the world. You're an expert in hieroglyphics
and a very important person. When an eroded, half legible stele is dug up inthe Egyptian sands, you
are the person the archaeologists will turn to to translate it.
But it's not inherently dificult to read hierglyphics fluently. The reason very few people can do it is that
there's not much of an employment market for it, and we don't have a cultural tradition of teaching
hieroglyphics at school. If you've got fluent Hebrew, then all you've got is what every five year old
Israeli child has already. Not particularly special. Though it's still essential to learn Hebrew if you are
serious about Old Testament scholarship.

Almost everyone does basic maths at high school, and the SATS are a mass test the covers that basic
curriculum. A perfect score qualifies you as a clerk. It also qualifies you to do futher study in a numerate
discipline, at a respected institution, which is the real point.

Charlie-Boo <shymathguy@gmail.com> writes:

> On Sunday, December 26, 2021 at 9:35:10 PM UTC-5, Ben Bacarisse wrote:
>> Charlie-Boo <shyma...@gmail.com> writes:
>
>> >> Citation please.
>> >
>> > See the 10th message in this thread.
>
> MESSAGE
> Charlie-Boo
> Dec 26, 2021, 7:17:01 PM

That's not how you cite Usenet posts either. I can't find any post with
that date, but there is one with the same number if minutes past the
hour:

Message-ID: <c4ee3fd0-c0f7-4795-aba4-04b3dc7a0d9bn@googlegroups.com>
Date: Sun, 26 Dec 2021 16:17:00 -0800 (PST)

but that contains only this:

A Mechanical Proof of the Unsolvability of the Halting Problem ~
Robert S. Boyer, J. Strother Moore

and that paper (Journal of the ACM, Volume 31, Issue 3, July 1984, pp
441–458, https://doi.org/10.1145/828.1882) does not appear to assert
what you call the Big Lie.

Am I looking in the wrong post or are you just citing any semi-automatic
proof in the hope that the authors say what you want them to have said?

>> If you had a paper or book that claimed that mathematics and computer
>> science have been automated, you'd just cite it.
>
> I have referred to a few - the Program Synthesis text, at least 2
> papers. These are the more famous ones.

No, you've given lots of vague references. No one appears to be
claiming what you want then to have claimed. And you certainly can't
ascribe that view to the whole field, much less to all of academic
computer science.

> Program Synthesis is the automation of computer programming.
> Automated Theorem-Proving is the automation of theorem-proving, a
> fundamental part of Mathematics.

Yes, we all know this. But I can't find anyone saying that mathematics
and computer science have been automated. That's why I am asking you
for an actual citation.

> Maybe you should talk more about the subject of this thread than the
> author of this thread.

The subject is boring. I don't think program synthesis is going
anywhere, and although I think there is considerable value in proof
assistants, you don't seem to be talking about them (since they are not
fully automatic). You seem to have invented the whole polemic yourself
just so you can have something to rail against.

--
Ben.

On Monday, December 27, 2021 at 9:19:53 AM UTC-5, Ben Bacarisse wrote:

> you've given lots of vague references . . . you certainly can't ascribe that view to the whole field, much less to all of academic computer science .. . . No one appears to be claiming what you want then to have claimed . . .. [the post] contains: A Mechanical Proof of the Unsolvability of the Halting Problem ~ Robert S. Boyer, J. Strother Moore and that paper (Journal of the ACM, Volume 31, Issue 3, July 1984, pp 441–458, https://doi.org/10.1145/828.1882) does not appear to assert what you call the Big Lie . .. . You seem to have invented the whole polemic yourself just so you can have something to rail against."

What is a "vague reference"? When did I refer to anything outside of Program Synthesis and Automated Theorem Proving, much less "all of academic computer science"? Even Donald Trump's Big Lie of persistent false election claims is not a reflection on every Republican or the party as a whole. It is only certain party leaders who are engaged in the attempted deception.

The Big Lie of academia is:

"Mathematics and Computer Science Have Been Automated"

The abstract begins, "A proof by a computer program of the unsolvability of the halting problem is described." They are saying that they have automated theorem-proving to the point of including seminal results from theoretical computer science. There are several other articles that make the same claim regarding other individual theorems. (I offered to dig up my collection.) The fact that the proof is not given, the method of deriving that proof is not given and only a single theorem is proven belies these claims. How could a theorem-prover only work for one theorem? How can they say it is described without giving the proof itself nor the method of its creation? Why aren't any new theorems proven? That is how theorem-proving works.

"The sceptic will say, 'It may well be true that this system of equations is reasonable from a logical standpoint, but this does not prove that it corresponds to nature.' You are right, dear sceptic. Experience alone can decide on truth." ~ Albert Einstein

The claims of having a Program Synthesis system are similar (see the recent text that I cited.) There are no examples of synthesized programs nor a procedure for producing them.

If what I say is true, then would a person who states these facts necessarily have "invented the whole polemic just to have something to rail against"? Even if it turned out to be false, how can one draw conclusions about the source of the belief or the personal motives of the author? How is that pertinent to a discussion of theoretical computer science and mathematics? That is merely arguing Ad Hominem and based on unknowable assertions about the author on top of it.

C-B
> --
> Ben.

Charlie-Boo <shymathguy@gmail.com> writes:

> What is a "vague reference"?

One that does not have enough detail for someone else to confirm what
you claim. No one asserts what you claim they do. Arguing against a
made-up claim is just a waste of time.

--
Ben.

On Monday, December 27, 2021 at 11:02:07 AM UTC-5, Ben Bacarisse wrote:
> Charlie-Boo <shyma...@gmail.com> writes:
>
> > What is a "vague reference"?
> One that does not have enough detail for someone else to confirm what
> you claim. No one asserts what you claim they do. Arguing against a
> made-up claim is just a waste of time.

Examples?

Is Program Synthesis the automation of computer programming?

Is Automated Theorem-Proving the automation of a fundamental part of mathematics?

C-B
> --
> Ben.

On Monday, 27 December 2021 at 16:09:45 UTC, Charlie-Boo wrote:
> On Monday, December 27, 2021 at 11:02:07 AM UTC-5, Ben Bacarisse wrote:
> > Charlie-Boo <shyma...@gmail.com> writes:
> >
> > > What is a "vague reference"?
> > One that does not have enough detail for someone else to confirm what
> > you claim. No one asserts what you claim they do. Arguing against a
> > made-up claim is just a waste of time.
> Examples?
>
> Is Program Synthesis the automation of computer programming?
>
> Is Automated Theorem-Proving the automation of a fundamental part of mathematics?
>
Ideally you should quote someone, preferably someone who has a reasonable standing
in the program synthesis / automated theorem proving community, and give a reference
for the quote.
Then explain why you disagree with what is being said.

On Monday, December 27, 2021 at 11:25:11 AM UTC-5, malcolm.ar...@gmail.com wrote:
> On Monday, 27 December 2021 at 16:09:45 UTC, Charlie-Boo wrote:
> > On Monday, December 27, 2021 at 11:02:07 AM UTC-5, Ben Bacarisse wrote:
> > > Charlie-Boo <shyma...@gmail.com> writes:
> > >
> > > > What is a "vague reference"?
> > > One that does not have enough detail for someone else to confirm what
> > > you claim. No one asserts what you claim they do. Arguing against a
> > > made-up claim is just a waste of time.
> > Examples?
> >
> > Is Program Synthesis the automation of computer programming?
> >
> > Is Automated Theorem-Proving the automation of a fundamental part of mathematics?
> >
> Ideally you should quote someone, preferably someone who has a reasonable standing
> in the program synthesis / automated theorem proving community, and give a reference
> for the quote.
> Then explain why you disagree with what is being said.

My statement is an aggregate of the claims of program synthesis and of automated theorem-proving. Each paper that claims to have a Program Synthesis system with no examples and procedure used to produce them is stating one part of the lie. Each paper that claims to have an Automatic Theorem-Proving system with no examples and procedure used to produce them is stating the other part of the lie.

The fact that nobody has produced either is my aggregate of all of these lies. Would you believe these claims without examples and a procedure by which they were produced?

I will pay $100.00 through the FIVERR.com website for a set of 3 nontrivial computer programs and automated procedure that produced them from nonprocedural specifications.

It is a lie because each claim is a lie. How can the lack of any examples or explanation of the methods used be explained any way else? Why would none of a hundred authors give a single example? The handful who claim an example don’t give a procedure by which it was produced. It is simply not credible. They write papers with new terminology and lots of formulas. But they leave out the program produced or explanation of how it is produced.

Isn't the proof in the pudding?

The reason we can combine the Program Synthesis nonsense and the Automated Theorem-Proving nonsense is that they share one important aspect: They are both about producing something tangible and familiar to the masses. It is one thing to make a claim about an abstract concept such as the Arithmetic Hierarchy. We can't see or create it. But computer programs and proofs of mathematics are objects we all have seen, created and/or used. They are shown to exist empirically.

So when someone claims to have a proof or computer program, you can ask to see it. It can be verified by personal examination. This is why it is easy to expose a false claim that a system produces proofs or computer programs. We can ask to see what it produces and how it was produced. And we can personally verify what it is.

C-B

On Monday, December 27, 2021 at 11:02:07 AM UTC-5, Ben Bacarisse wrote:
> Charlie-Boo <shyma...@gmail.com> writes:
>
> > What is a "vague reference"?
> One that does not have enough detail for someone else to confirm what
> you claim. No one asserts what you claim they do. Arguing against a
> made-up claim is just a waste of time.

"Program synthesis is the mechanized construction of software."

Program synthesis: challenges and opportunities
Cristina David - University of Cambridge
October 2017Philosophical Transactions of The Royal Society A Mathematical Physical and Engineering Sciences

"A proof by a computer program of the unsolvability of the halting problem is described."

A Mechanical Proof of the Unsolvability of the Halting Problem
Robert S. Boyer, J. Strother Moore
Journal of the ACM, Volume 31, Issue 3, July 1984, pp 441–458, https://doi.org/10.1145/828.1882)

> --
> Ben.