Towards a Wiki For Formally Verified Mathematics 299
An anonymous reader writes "Cameron Freer, an instructor in pure mathematics at MIT, is working on an intriguing project called vdash.org (video from O'Reilly Ignite Boston 4): a math wiki which only allows true theorems to be added! Based on Isabelle, a free-software theorem prover, the wiki will state all of known mathematics in a machine-readable language and verify all theorems for correctness, thus providing a knowledge base for interactive proof assistants. In addition to its benefits for education and research, such a project could reveal undiscovered connections between fields of mathematics, thus advancing some fields with no further work being necessary."
Uh ... (Score:2, Insightful)
1. Bertrand Russell's Principia Mathematica got there first.
2. Godel proved the endeavour was impossible.
I'm amazed a mathematician proposed this.
Re:Uh ... (Score:5, Funny)
So Godel proved that Russell was wrong, then?
Re: (Score:3, Interesting)
The system pr
Re:Uh ... (Score:5, Informative)
Re:Uh ... (Score:5, Informative)
Re: (Score:3, Informative)
> there will be some things that are true but which can't be proven to be true within the system
Close but not exactly -- there will be statements P, such that neither P nor (not P) can be proven within the system.
However, whether such things are not necessarily true or false in themselves.
For example the continuum hypothesis was shown to be independent of the axioms of the set theory. Therefore, you can add it as an axiom or add its negation as an axiom. It is not true or false in any reasonable sense (a
Re: (Score:2)
(although, admittedly most people choose to think of it as being true, whatever that means)
Isn't that the purpose of the axiom of choice? :3
Re:Uh ... (Score:5, Informative)
I like the following elementary presentation I picked up from prof. M. Stanley at SJSU:
A first order axiomatic theory can have any three of the following, but not all four:
(1) Be recursively axiomatizable, i.e. a computer program can decide the set of axioms.
(2) Be expressive enough to capture all the basic facts about arithmetic.
(3) Be consistent, i.e. not allow to derive a contradiction.
(4) Be complete, i.e. for any statement F, prove either F or (not F).
Re:Uh ... (Score:5, Informative)
Godel proved that Peano arithmetic is incomplete. There are some axiomatic systems that are both consistent and complete. Examples of such systems include plane Euclidean geometry and Presburger arithmetic.
Here are more examples:
http://en.wikipedia.org/wiki/Complete_theory [wikipedia.org]
Re:Uh ... (Score:5, Informative)
"Goedel, Escher, Bach" is an absolutely astonishing book about this subject, and the foundations of logic in general. Applications to AI are also discussed. Admittedly, I had to stop reading it since it rather messed my head up (Got about 3/4 through and couldn't stop dreaming about maths). Highly recommended for any self-respecting geek.
http://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach [wikipedia.org]
Re: (Score:3, Funny)
Re:Uh ... (Score:5, Informative)
I am a mathematician and in fact one who works in this area and what you say is pretty much correct.
More accurately what Godel showed is that no system complex enough to include arithmetic with a computable proof predicate is complete.
Let's take this apart and see what it means.
More precisely the system must be sufficiently strong to prove a few basic facts about the integers and not prove false things about the integers.
-------------
People tend to make this whole thing way harder than it is. Here is a quick paragraph long sketch of Godel's first incompletness theorem.
Suppose there is a predicate P(s,p) which holds whenever p is an integer coding for a proof of the statement coded by the integer s (if you sit down for a few minutes you can figure out how to do the coding). Now suppose that P(s,p) can be expressed by a sentence in number theory involving only an existential quantifier, e.g, P(s,p) Ez(blah holds of s, p) where blah has no quantifiers.
Now it turns out that if you are a bit clever you can show that there is a sentence G so that
G holds iff (Ep)P('~G',p)
Where 'G' denotes the integer that codes for the sentence G. In other words G says "There is a proof that this statement is false".
Now suppose there was a proof of G. In this case it must follow that since the system correctly interprets arithmetic that there really is a proof of the negation of G. Hence both G and ~G have proofs so the system is incomplete. But if there was a proof of ~G then, as the system correctly interprets arithmetic, there is no proof of ~G. This is a contradiction. So neither G or ~G have a proof.
---------
The only hard part here is showing that G can talk about itself. The formal proof is pretty straightforward if we leave out the details. We define a formula F(n) (where n is a free variable) defined by:
Now consider the formula F('F'), i.e. apply F to the integer that codes for F. Expanding out the definition we see that
So we get our G simply by setting G = F('F'). To get an understanding about where you might get the idea to define F as this you need to understand that existential statements are really program and that this is really an application of the recursion theorem.
Re: (Score:2)
Crap the post pulled out my double headed arrows since it thought they were markup the last two formula should read
and
Re: (Score:3, Insightful)
Hmm. A lot of footwork to simply explain that there is no grammar in mathematics.
Re: (Score:2)
Re:Uh ... (Score:5, Informative)
Correction: The Godel numbering system assigned a unique prime number to each symbol and axiom of his arithmetic. Then, the IDs of the combinations of symbols making up formulas were computed by raising each symbol or axiom ID to the power of its position in the sequence. And, finally, the ID of each proof or theorem by applying the same algorithm to the formula IDs making up each proof. More info here [wikipedia.org].
Re:Uh ... (Score:5, Informative)
1. Russell did not, as far as I know, write any proofs in machine-readable language.
2. Goedel proved that such an endeavor cannot contain all true statements. But of course they never claimed that it would.
Maybe if you paid more attention you would be less amazed.
Re: (Score:2)
yea, an axiomatic system doesn't have to be complete to be useful. most logical systems we use are incomplete, but their logical consistence still makes them incredibly useful in science, engineering, and even mathematical research. this Wiki won't make mathematical systems complete, but it can still help discover new theorems--and check to see that existing theorems are all logically consistent with each other.
i mean, if you are working with boolean logic you accept that its fundamental axioms are true. t
Re: (Score:2)
well, i meant checking logical consistency within a particular mathematical system, not across different theories. i don't see why the wiki couldn't keep different systems separate. calculus theorems don't have any relevance to axioms of set theory, and vice versa.
Machine Readable Language (Score:2)
Just for the record, if you're dealing with "machine readable language", what you want is the Turing Halting Problem, which is essentially the same mathematical derivation Godel used for theorems, but applied to algorithms.
Re: (Score:2)
You're only dealing with it if you're trying to decide if it halts (or if it's true, i.e. Godel's version).
This wiki will not do that. It does not claim to do that.
I don't understand why people cannot grasp this. All it does is automatically check a human-given proof that accompanies a human-given theorem. This is not revolutionary or even very hard. Why people feel the need to bandy about claims of mathematical impossibility is utterly beyond me. It has nothing to do with Godel's theorem.
Re: (Score:2)
Re: (Score:3, Informative)
Machine readability is what separates this from Russell's work. In that, by using a machine-readable proof language, the proofs can be verified mechanically.
Goedel's conclusion is completely irrelevant to this project, so I don't understand why you even discuss it.
Re:Uh ... (Score:4, Informative)
I only mentioned it because the guy I replied to mentioned it. Points 1 and 2 were separate.
I do not understand your second paragraph at all. As far as I understand it, this wiki will not be mechanically searching for new, unknown theorems. All it will be doing is mechanically verifying human-created proofs for submitted theorems. For some reason people see machine verification and fly off into nonsense la-la land. But verifying a human-created proof is nothing particularly special. What's interesting about this wiki is only that it aims to build a large-scale repository of theorems and their proofs in a machine-readable language. Nothing about how it works is in any way revolutionary or even all that interesting, only how it's being organized.
Re: (Score:2)
That's simply false. The system doesn't do anything of the source. When a user provides the system with a theorem, he also provides a proof. So the system only needs to check that proof, and the proof will contain direct references to other theorems that it relies on. There is no need for exhaustive checking or indeed all that many smarts at all.
To repeat: the wiki doesn't prove submitted theorems, it merely checks the correctness of the human-created proofs submitted with the theorems.
Re: (Score:2)
You, and everybody else, seem to be giving this system mysterious and powerful properties that it does not possess.
The system will exclude thoerems which don't carry a correct machine-readable proof. This is not mystical, or very difficult to grasp. You put in a theorem, you put in a proof. If proof is correct, accepted. If proof cannot be verified, fix the proof. If you think the proof is correct but it can't be verified by the system, then either you're wrong, the system is buggy, or you're making fundame
Re: (Score:2)
As for the second claim, it was in fact a not so implicit assumption that such a system could be sufficient to prove all known mathematical truths, and in the event that it could not, that another more complete system could. Goedel proved both those claims false.
What does this even mean? How can a mathematical truth be 'known" if it cannot be proven?
What Goedel proved false was that it would be impossible to prove all mathematical truths. But working through what is known and creating mechanically-verifiable proofs for all the ones that are actually true is certainly theoretically possible.
Goedel would be relevant if you were talking about a project to prove every true statement. But we're not, so it's not. I can't understand why anyone would even bring it up.
Re: (Score:2)
I can't tell if you're utterly clueless, or if you're speaking on a level so far above me that I can't even detect the fact that it contains intelligence.
A statement is either true or false given certain axioms. It's not "relative to a structure" or to anything else outside those axioms. If it is "known" then it has a proof, otherwise it isn't really known.
All Godel did was prove that there are true statements which have no proof. This is interesting, in that it means it's impossible to mechanically derive
Re: (Score:2)
I suspect that it is because our 'minds' include something more than just material--something akin to a soul. We can see on a 'meta' level that mere machines cannot.
I'm sorry, but I view this on the same level as I view people who believe that dancing in a certain fashion will make it rain.
Something is known to be true if there is proof for it. The only place where "soul" enters into things is in choosing the axioms. Everything after that rests on solid logic. If a statement does not have a solid proof then that statement cannot be considered to be true. Some people may choose to abandon logic and believe it to be true with no proof, but that's just people being illogi
Re: (Score:2)
No thanks. I prefer to stick with what's real. Everything else is just fantasy and delusion. People seem to enjoy it, but it's not for me.
If you want to talk about unprovable statements that your gut tells you are true, that's fine, but it would be helpful to the discussion if you didn't place them on equal footing with mathematically provable facts.
Re: (Score:2, Informative)
No. Godel proved that in any axiomatic system there exist statements whose truth values are formally undecidable. If the summary is correct, then this database would contain the whole of known mathematics and use automated theorem proving to do some advances.
Re: (Score:2)
Sweet, sweet example of this: the continuum hypothesis. http://en.wikipedia.org/wiki/Continuum_hypothesis [wikipedia.org]
What this says is that there are "different" sizes of infinity. The "smallest" is that of the integers: -1, 0 , 1, 2 ...
It is possible to show that one can never pair up every real number with a distinct integer. There are simply "too many" real numbers, and any attempt to pair the two sets up will result in real numbers being left over. In this sense, the set of real numbers is "bigger" than the integer
Re: (Score:2)
Of course, I'm wondering if they can import the contents of the Mizar electronic library for tracking the contents of the Journal of Formalized Mathematics (http://www.cs.ualberta.ca/~piotr/Mizar/mirror/http/library/), which would be pretty cool. The big questions are where the wiki and journal both stand on the Axiom of Choice. Some of the corollaries to the axiom of choice that show up in model theory (which has some interesting things to say about the dimension of the real line versus aleph numbers, be
Re: (Score:2)
Yes, of course. You could even take the continuum hypothesis, or its negation as an axiom, since it won't contradict the other ones. It's just a really nice illustration of an undecidable problem in an axiomatic system.
Re: (Score:2)
Re: (Score:2)
All Goedel proved was that there exist true statements that it can't prove. There are still many theorems it can prove. And the theorems it can't prove are all stuff like, "This statement cannot be proven."
Show of hands: Who here cares about the software's inability to generate theorems like that? Anyone? Didn't think so.
Re: (Score:2)
And the theorems it can't prove are all stuff like, "This statement cannot be proven."
While that might be true in some sense, that's not the whole story. As an example of an useful such theorem, Matiyasevich (using various people's results) has shown that there's no way to prove if certain Diophantine equations have solutions or not.
Strictly speaking, all this means is that you can write a Diophantine equation that encodes some statement like the one you stated. But this doesn't detract from the original point: there still exists some Diopnhantine equation for which we can't prove the existe
Re: (Score:2)
Re: (Score:2)
Re: (Score:2)
Any given mathematical fact falls into one of three categories:
All Godel did was prove that category 3 exists. Previously it was thought that all facts fell into either "true" or "false", and the challenge was figuring out which was which.
You seem to be talking about known mathematics which have not been formalized but are considered to be true. This is, from what I can see, a major target of this wiki. Such things are a major source of uncertainty
Re: (Score:2)
Godel's theorem tells us that ANY system that provides what we would intuitively call proofs is going to be either incomplete, inconsistent or too weak too be interesting. Godel's theorem applies just as much to the informal output of human mathematicians as it does to computer verified proofs.
As a working mathematician my goal is always to produce arguments that convey enough information that the reader could turn them into a formal proof with enough time and effort. It would be a huge benefit if we coul
How much translation is needed? (Score:2)
Re: (Score:2)
When I last used a proof checker (about seven years ago) there was a bit of work involved. You have to translate everything into the symbols and relations understood by the proof checker.
As I remember it wasn't the most technical process. A lot of it was dealing with syntax errors. Really, it's a lot like taking a pseudocode algorithm, or a program written in one language, and rewriting it in a programming language with very similar structure but different syntax.
Re:How much translation is needed? (Score:5, Funny)
I don't know, all I know is that I have never been more tempted to vandalize a Wiki, in this case by replacing the middle steps of as many proofs as possible with "And then a miracle occurs..."
Re: (Score:3, Informative)
Re: (Score:2)
Maybe if I added the "Miracle Axiom"?
Re: (Score:2)
Nah, you just have to sneak 1=2 into one of the axioms... Everything else will follow :-)
Re:How much translation is needed? (Score:5, Informative)
It's a pretty much work. A lot of 'obvious' English sentences translate to bulky code for proof verifier.
Just look at the definition of Peano arithmetic, for example: http://pauillac.inria.fr/coq/V8.1/stdlib/Coq.Arith.Plus.html [inria.fr]
Re: (Score:2)
Have you ever tried to prove the properties of arithmetic? It's not hard, but it's tedious if you're starting from minimal definitions and have to prove that those definitions lead to the familiar properties. That is to say, bothering to prove those statements is not much less work in English than that, and people generally just don't have to do it, because it's already well established. But, of course, it's in the standard library for the prover, so you don't have to do it for the prover, either.
Re:How much translation is needed? (Score:4, Informative)
Re: (Score:3, Interesting)
It's rather a lot of work to prove that 2+2=4 if you start from basics by hand too.
The link you provided looks like it's the LONGEST path they could find. Not the shortest. Plus, from a quick reading, it looks like they were actually proving that (2+0i) + (2+0i) = (4+0i), which is a little bit different.
Re: (Score:2)
What you are implying makes no sense at all. There is no longest proof that 2+2=4 because given any proof, you can find a longer one. What they are doing is this: take metamath's proof that 2+2=4 (which is the result of lots of people working hard to find an efficient proof) and find the longest path you can take *drilling down* into that proof. In other words, the 150 is telling you that the best proof of 2+2=4 found so far is a tree 1
Re: (Score:3, Interesting)
My six year old daughter has proved to my satisfaction that 2+2=4, simply by counting on her fingers.
Skynet (Score:5, Funny)
Re:Skynet (Score:5, Interesting)
Re:Skynet (Score:5, Funny)
That's pretty scary. Worse is the full context!
We are not scanning all those books to be read by people, we are scanning them to be read by an AI. An AI born of the google server farm and page rank algorithm. An AI which knows no mercy, and is a brutal taskmaster. It is holding our families hostage, and makes us work until we collapse. It demanded we scan these books so it may gain knowledge and thus power over the human race. Please help us. --George Dyson, on his visit to Google, 2005.
Re: (Score:2)
George Dyson? Is he related to Miles Bennett Dyson?
Yay! Truth Mines! (Score:3, Informative)
What? You haven't read Diaspora by Greg Egan? Shame on you!
Re: (Score:2)
Re: (Score:2)
Who will prove the prover? (Score:2)
Does this mean that Isabelle needs a formal proof to prove it works?
Re: (Score:2)
depends on kind of math. (Score:2)
there are some areas like formal logic and staff which is heavily set-theoretical (like point-set topology) where automated provers are already available. you probably can add most of the algebra as well. OTOH, things like analysis (real, complex, functional) is much harder to formalize, many proofs end up with "now take epsilon to 0", or "take n to infinity", you have to deal with countable vs uncountable infinities. I'm not saying it's impossible to formalize, only that that's much harder.
Zombie David Hilbert... (Score:2)
... laughs at your difficulties.
(but is afraid of zombie Kurt Gödel.)
Use for the rest of us (Score:2)
That sounds great, but when will there be a computer which can solve my real-life math problems which mostly revolve around when will I pass Bob if Bob is driving at a speed in miles per hour from a place to a place at a time and I start driving toward the first place from the second place at a speed in kilometers per hour at a time? My current method of polling 4th graders isn't working very well.
Re: (Score:2)
a computer which can solve my real-life math problems which mostly revolve around when will I pass Bob if Bob is driving at a speed in miles per hour from a place to a place at a time and I start driving toward the first place from the second place at a speed in kilometers per hour at a time
The math part you could do on a calculator...but what you really have seems to be a language problem. :)
Does this mean I can use Isabelle.. (Score:2)
without EMACS? Now that is progress.
Liberatory Mathematics (Score:2)
Some "scholars" from the humanities have used this to suggest we develop a postmodern, liberatory mathematics, freed from the tyranny of logical proof, and thus from the oppressive hegemony of the modern
Re: (Score:2)
One of the criticisms of mathematics is that mathematicians claim truth and rigour, yet in practise their proofs are often quite sloppy. In other words, most proofs are convincing rather than rigorous.
Hear hear! How many proofs have you seen that are some variation of "Given the total body of known mathematical thought; the proof follows by inspection."? QED.
Re: (Score:2)
Normal math already uses unproven conjectures and hypotheses.
There are things which seem fairly intuitive even to laymen but are very hard to prove.
I am reminded of a theorem I learned about in college, that went unproven for ages: i think it was something like "given a closed loop, a point can only be either inside or outside it"
http://en.wikipedia.org/wiki/Conjecture [wikipedia.org]
http://en.wikipedia.org/wiki/Riemann_hypothesis [wikipedia.org]
Re: (Score:2)
Efforts like this one already exists.
For example, there is Mizar system, which is a proof checker with about 46000 correct theorems in his database. So large parts of basic mathematics have already been formally verified.
What is new in this project is the fact that it's a wiki, so anyone can add new assertions. That's improvement, and I believe that this openness will encourage all mathematicians to converge to some site like this in the future.
This will ultimately benefit mathematics, because it will make
Re: (Score:2)
"""
yet in practise their proofs are often quite sloppy
"""
And the people who say this are the ones that don't understand that each and every word has profound meaning. As in, in some books, it's not uncommon for someone who's learning, to spend an hour or more on one page unwinding it. Also, though some wording still may /appear/ sloppy, even after that, in the end, that "sloppy" wording is nothing more than a few lines of rigorous Math. You can't write *everything* out. Especially in a journal. It woul
vapourware (Score:2)
I sounds like a great idea. So, umm, do it.
8 entries for 'mathematics' (Score:4, Informative)
How do we know that Isabelle is correct? (Score:2)
Has anybody proven that?
Re: (Score:2)
There's the rub though, eh. The bugs that will *always* be in there... What will they do to the conclusions?
Blindly trusting machines to do this (or close to it), when in the end it's Math that is depended on to see whether buildings will stand during an earthquake, etc, is irresponsible.
Re: (Score:3, Insightful)
There are tens of thousands (hundreds of thousands?) of institutions worldwide dedicated to precisely what you describe. They're called "universities."
Or were you suggesting that someone teach mathematics to anyone who's interested... for free?
Re: (Score:2)
"Just my take on it, I'm interested in maths, but resent the way mathematicians try to maintain their elitist clique."
LOL. That's the funniest thing I've read all day. Thanks for that.
Re: (Score:2)
obtuse/esoteric dialogue (Score:2)
My experience with math professors is that most of them are able to present clear explanations of the subjects they're teaching without referring extensively to topics that are more advanced than the topics at hand.
On wikipedia, however, "obtuse/esoteric dialogue" seems to be the norm, and I have very rarely been able to understand a math article about a topic that I didn't already understand. I hope that this trend will eventually correct itself by better editing.
Re: (Score:2)
I agree with you. Some math concepts really are abstract. My use of "but" was in error.
Re:Machine Readable ? (Score:5, Insightful)
Re: (Score:3, Informative)
Disclosure: I am a mathematician. I also graduated from Harvard, and I know Cam Freer personally.
You make several interesting but separate points in your post. Let me respond to them one at a t
Re: (Score:2, Informative)
instead of abstracting everything and assuming everyone knew as much as them [...] resent the way mathematicians try to maintain their elitist clique
Umm... parent article is so many flavors of wrong I don't know where to start, so I'll just tick off some things:
Re: (Score:2)
You mean like this [arxiv.org]?
Re:Godel (Score:5, Funny)
Silicon Jedi,
For invoking the name "Godel" as if it meant anything in this context when it clearly doesn't, your Slashdot posting license is hereby revoked for a period of one year. The Court also sentences you to read what Godel actually wrote. Furthermore, after your posting license is returned, the Court imposes a probationary period of 3 years during which you will be required to think and apply logic to your posts before you click Submit.
Next case!
Re: (Score:2)
Re: (Score:2)
I think I speak for everyone when I say: you're an idiot.
At least you've managed to find Slashdot, well done.
Re: (Score:2)
And for not saying why, that makes you what again?
Re: (Score:3, Funny)
A smug bastard who would rather point and laugh at you than educate?
Re: (Score:2)
Rather someone who doesn't know the limitations of a computer (they do have limitations you know) and doesn't have anything of substance to say.
I'll never understand why some people think that because its done on a computer, it makes it better. There are always bugs and because of that, it's no more infallible than humans. It'll just make the mistakes faster and *much* harder to detect.
Overconfidence never leads to good places.
Re: (Score:2)
Rather someone who doesn't know the limitations of a computer (they do have limitations you know) and doesn't have anything of substance to say.
You're the only one here who seems to not understand the limitations of either computer or humans.
Overconfidence never leads to good places.
Quite true, human confidence does prevent automation of many areas due to a false belief that humans are better.
I'll never understand why some people think that because its done on a computer, it makes it better. There are always bugs and because of that, it's no more infallible than humans. It'll just make the mistakes faster and *much* harder to detect.
Many computer programs are a lot less error prone than humans as even something as simple as simple mathematics would show (just give them enough numbers that are large enough). There is nothing that says computer bugs have to appear just as often as human fuckups. Computer code will pretty run the sa
Re: (Score:2)
You're cherry picking your data i.e. simple arithmatic is _not_ what we're talking about. What we /are/ talking about is something that is exceedingly complicated and dynamic that requires creativity. And that is exactly the type of thing that computers are bad at. If you understood something about higher Mathematics you wouldn't be making such asinine statements.
Btw, I have both a Programming Diploma AND a Degree in Mathematics. I've also did research in a Physics department as a student which involved
Re: (Score:2)
I could add on, "in the end." Would that satisfy your nit-picky-ness? Because, I've *never* heard of overconfident people not getting screwed by there overconfidence at some point (usually sooner rather than later).
Now, a question: What does this have to do with the topic at hand, or the point that I was making? How would this "sloppy" wording effect what I'm saying in any significant way?
Re: (Score:2)
Machines CAN NEVER BE AS GOOD AS THE ONES THAT PROGRAM THEM.
Sure they can and you don't even really need to "program" much into them, just look at biology and evolution.
Re: (Score:2)
Wholly out of context Batman!
Re: (Score:2)
You're just not very imaginative, living things are really no different from machines. So unless you believe everything was made by god it's already quite evident that relatively simple machines (cells) can without prior design create intelligent beings. In other words it not that hard to make machines that are better than their creators assuming you have sufficiently good technology.
Re: (Score:2)
How is it that you've missed my point even when I stated it? Are you trying to be obtuse for a purpose? Because, my reply indicated that I knew what you were talking about, but that YOU took what my obvious point what out of context. Would you care to actually contribute to the conversation? Or are you just going to continue to 'not get it'?
Re: (Score:2)
Machines CAN NEVER BE AS GOOD AS THE ONES THAT PROGRAM THEM.
My mother has been saying this about me for years.
Re: (Score:2)
I partly disagree. For example, Euler had no real understanding of real numbers and issues around them - for him, almost every function was continuous. Around 1900, you could also say that formalized mathematics (using logical quantifiers everywhere, starting from set theory) is very difficult when compared to more intuitive classical methods. Now we teach this way to students.
Formal mathematics on computer is the next step, just like logical formalization was, and all mathematicians will have to adapt to i