sometimes i wonder if i should be a mathematician at all .. lately i've been reminiscing about the dreams my younger self had: among them was to be a successful novelist, perhaps in science fiction.
so when i read news articles like this one ..
.. then i immediately begin to imagine the possibilities:
if the strength of a computer lies in being very efficient with a finite, fixed set of tools, then imagine if we could get computers to prove simple lemmata for us, just by giving them suitable hypotheses and a fixed set of axioms and existing lemmata ..
yes, it is hard enough to build a robust proof-checking program .. and some researchers have spent years of their lives focusing on a single, specific verification .. but i'm not talking about a universal engine:
i liken it to writing programs that play go or chess well. it's not that the computer can think on its own, but rather that it can traverse through the decision tree of possible games very efficiently. in fact, a competitive program mightn't even run through all the possibilities, but simply the games that grand masters have played before.
so imagine coding in all the basic, rigorous proofs from mathematics (e.g. the proof of the triangle inequality in Euclιdean space) and adding shortcuts into the space of all proofs. i wonder what lemmas a computer could tell me ..?
being a mathematician, sometimes i have mathematical daydreams.
so when i read news articles like this one ..
"Some might argue that computers will never be able to match human ingenuity but it is difficult these days to argue they can't at least mimic many of our skills.
Take the eDavid painting robot. The computer-controlled arm - adapted from a welding machine - chooses from five brushes and 24 colours to create impressive artworks on canvas.
It works by snapping a photo of its subject matter and then making the necessary calculations to turn the image into a drawing or painting in a wide variety of styles.
Its creators admit that it has no awareness of what it is doing. But it is able to make decisions about things like shading and brushstrokes as it goes, tweaking its moves based on how the picture is evolving, rather than just creating a pre-determined image."
~ from "The quest to turn computers into creative artists" @bbc_tech
.. then i immediately begin to imagine the possibilities:
if the strength of a computer lies in being very efficient with a finite, fixed set of tools, then imagine if we could get computers to prove simple lemmata for us, just by giving them suitable hypotheses and a fixed set of axioms and existing lemmata ..
yes, it is hard enough to build a robust proof-checking program .. and some researchers have spent years of their lives focusing on a single, specific verification .. but i'm not talking about a universal engine:
i liken it to writing programs that play go or chess well. it's not that the computer can think on its own, but rather that it can traverse through the decision tree of possible games very efficiently. in fact, a competitive program mightn't even run through all the possibilities, but simply the games that grand masters have played before.
so imagine coding in all the basic, rigorous proofs from mathematics (e.g. the proof of the triangle inequality in Euclιdean space) and adding shortcuts into the space of all proofs. i wonder what lemmas a computer could tell me ..?
being a mathematician, sometimes i have mathematical daydreams.