Stupid Patent Of The Month: A Patent On Using Mathematical Proofs

from the break-out-your-wff-'n-proof dept

Fri, Nov 30th 2018 7:39pm — Joe Mullin and Daniel Nazer

In some fields, software bugs are more than the proverbial pain in the neck. When software has to ensure that an airplane lands safely, or that a pacemaker keeps operating, there's no room for error.

The idea that mathematical proofs could be used to prove that software is error-free has been around since the 1970s, and is known as "formal verification." But like a lot of technologies that some visionaries saw coming, it took time to develop. In recent years, computing power has become cheap enough for formal verification to become practical for more software applications.

Unfortunately, last month, the field had a monkey wrench thrown into it, in the form of U.S. Patent No. 10,109,010, which the patent office awarded to a U.K.-based company called Aesthetic Integration Ltd.

Claim 1 of the patent describes creating mathematical "axioms"—formal mathematical statements—that describe a computerized trading forum. The patented method then describes analyzing, with a "computer assessment system … the mathematical axioms that describe the operation of the trading forum." In other words, the patent describes using formal proofs to check for bugs in a "computerized trading forum." It's formal verification—just applied to the financial services industry.

Of course, Aesthetic Integration didn't invent formal verification, nor did the company invent the idea of software powering a "trading forum." The company has apparently created software that utilizes formal verification in the financial services space, and that software might be perfectly good. But the Patent Office has effectively allowed the company to patent a whole sector of formal verification.

To be fair, the '010 patent appears to reflect some advanced and difficult programming by Aesthetic Integration. But that does not mean it should be patentable. Consider the following analogy: there are no 50 story buildings in Cincinnati. Building a 50 story building in Cincinnati, and making it compliant with seismic safety standards, would be hard work. It would take many engineers a great deal of effort to apply existing techniques to complete the project. You could write a lengthy paper describing that process, which might include lots of complex charts and diagrams. Still, that does not mean a company that completes such a project should then get a monopoly on tall buildings in Cincinnati.

Aesthetic Integration claims to be the first to apply formal verification to trading software. If that's true, the company may get a well-earned competitive advantage by being the first to this market. But it should not get a 20 year monopoly simply for applying programming techniques that the company itself has described as part of a "mature and effective field of science."

Ultimately, the '010 patent reflects a broader problem with Patent Office's failure to apply a meaningful obviousness standard to software patent applications. We have explained before that the Patent Office is all too willing to hand out patents for using known techniques in a particular field. Flow charts and whirligigs can make a concept look new when it isn't—especially when a patent owner fills its application with obscure language and "patentese." The Federal Circuit has also encouraged this through its hyper-formalistic approach to obviousness. The end result is an arms race where people rush to patent routine software development.

As we've said before, patents are simply a bad fit for software. The Patent Office should stop giving out patents on formal verification, or other well-known software processes.

Republished from the EFF's Stupid Patent of the Month series.

Thank you for reading this Techdirt post. With so many things competing for everyone’s attention these days, we really appreciate you giving us your time. We work hard every day to put quality content out there for our community.

Techdirt is one of the few remaining truly independent media outlets. We do not have a giant corporation behind us, and we rely heavily on our community to support us, in an age when advertisers are increasingly uninterested in sponsoring small, independent sites — especially a site like ours that is unwilling to pull punches in its reporting and analysis.

While other websites have resorted to paywalls, registration requirements, and increasingly annoying/intrusive advertising, we have always kept Techdirt open and available to anyone. But in order to continue doing so, we need your support. We offer a variety of ways for our readers to support us, from direct donations to special subscriptions and cool merchandise — and every little bit helps. Thank you.

–The Techdirt Team

Filed Under: math, patents, proofs, stupid patent of the month

19 Comments

If you liked this post, you may also be interested in...

Reader Comments

Subscribe: RSS

View by: Time | Thread

Gary (profile), 30 Nov 2018 @ 8:49pm

Seems legit
Sure, the ancient greeks invented axioms - but these guys were first to file!
[ link to this | view in thread ]
OGquaker, 1 Dec 2018 @ 2:35am

Can't let some fool go off half-cocked
Half of what NASA 'invents' is behind a NASA 'patent', so they control development, or not. AND, almost 0.0 of their IP/patents has Not been covered by six decades of prior art ...I have been reading all of their LATEST endless patent breakthroughs, with tax dollars, since the 1980's. Just subscribe to https://www.techbriefs.com/
[ link to this | view in thread ]
hij (profile), 1 Dec 2018 @ 5:09am

How is this new?
There is plenty of prior art for the application of formal systems in verifying algorithms. See for example MIT's PS+SE group. Software to verify formal logic systems has been in use for a long time now, and formal systems has been a focus of academic research for well over a decade. The software of evaluating formal systems is well known, and the hard part is developing the system of formal logic to define a problem in question.
[ link to this | view in thread ]
Anonymous Coward, 1 Dec 2018 @ 7:19am

Re: Can't let some fool go off half-cocked
Please explain how the government holds a patent.
[ link to this | view in thread ]
sparkydoc (profile), 1 Dec 2018 @ 7:21am

Stupid patents
I propose a new party game of trying to come up with a patent stupid enough to be rejected by the patent office. For instance: a gaseous mixture of 78% nitrogen,21% oxygen, 1% argon, and trace amounts of other gases, suitable for sustaining metabolism, inflating objects, and other applications. Once air is patented I could make a fortune!
[ link to this | view in thread ]
Anonymous Coward, 1 Dec 2018 @ 7:30am

I think we found out_of_the_blue, guys!
[ link to this | view in thread ]
Feldie47 (profile), 1 Dec 2018 @ 9:29am

My name is Pyth A. Goras. I have discovered that the squares of the two legs of a right triangle are equal to the square of the third side. I am requesting the U.S. patent office issue me a patent.

Now I'm going to sue everyone who constructs right triangles: Lego, architects, artists, contractors...

All right triangles are MINE! MINE! MINE!

Idiocy rules!
[ link to this | view in thread ]
Al Gore-rhythm, 1 Dec 2018 @ 2:23pm

Re:
And all INCORRECT triangles are mine!!! :)
[ link to this | view in thread ]
bhull242 (profile), 1 Dec 2018 @ 4:47pm

You know, I’ve heard people compare software IP to banning maths, but this is as close as I’ve seen someone patenting math.
[ link to this | view in thread ]
Anonymous Coward, 1 Dec 2018 @ 5:39pm

Re: Stupid patents
A liquid composed of dihydrogen monoxide suitable for drinking.
[ link to this | view in thread ]
Anonymous Coward, 1 Dec 2018 @ 5:49pm

Re:
I have discovered that C^2 = A+^2 + B^2 - 2ABCos(theta). My patent is broader and includes your specific case.
[ link to this | view in thread ]
feldie47, 1 Dec 2018 @ 7:16pm

Re: Re:
Actually your discovery is a derivative of mine. Your trig slight of hand doesn't arrive for hundreds of years. That nonsense will just add thousands to the inevitable lawsuit!

Pyth A. Goras

(and the fact that some Asians knew about this 3,000 years before me is irrelevant)

Mine, mine, mine,mine.
[ link to this | view in thread ]
Col Minor, 1 Dec 2018 @ 8:59pm

Re: Re: Re:
Sorry, but I patented mine mining already. And also mining mines, because you can't mine a mine , or be mining a mine without infringing on that mine-mining mining-mine patent o'mine, if you don't mind.

So only I can mine that mine-mining.

Got it? Mine-mining? Mine!!!
[ link to this | view in thread ]
Darkness Of Course (profile), 2 Dec 2018 @ 12:37pm

Re: Oh no it isn't
Look into https://en.wikipedia.org/wiki/Diamond_v._Diehr

Diamond v Diehr, yup. Patent on math, 'running on a computer' so a double whammy.
[ link to this | view in thread ]
Anonymous Coward, 3 Dec 2018 @ 7:14am

Re: Re: Can't let some fool go off half-cocked
Presumably they file for them, like anyone else. NASA has some, as does the NSA.
[ link to this | view in thread ]
Anonymous Coward, 3 Dec 2018 @ 7:14am

Re: Re: Re:

(and the fact that some Asians knew about this 3,000 years before me is irrelevant)

True, the USA is a first-to-file system.
[ link to this | view in thread ]
Anonymous Coward, 3 Dec 2018 @ 8:24am

Re: Re: Re: Can't let some fool go off half-cocked
No, they don't.
[ link to this | view in thread ]
Pref Anon, 3 Dec 2018 @ 11:25am

Re: Re: Stupid patents
Just remember someone patented a stick
[ link to this | view in thread ]
Boba Fat (profile), 6 Dec 2018 @ 1:14pm

To promote the progress of science and useful arts
Obviously, anything that exists anywhere PLUS teh internets is progress and therefore patentable.
[ link to this | view in thread ]