Start a hangout

## Profile

Andrej Bauer

Works at University of Ljubljana

Attended United World College of the Adriatic

Lives in Ljubljana, Slovenia

761 followers

AboutPostsPhotosVideos

## Stream

### Andrej Bauer

Shared publicly -The evil publishers are dying slowly but surely. Here is another nail in the coffin. The important thing is not the book itself, but the technology around it (it's a

**configurable**textbook where you get to choose what to include and what notation it should use!) and the fact that it has been done at all.We’ve kept this on the down-low long enough, I think: together with Aldo Antonelli, Jeremy Avigad, Nicole Wyatt, and Audrey Yap, I’ve been working on an open source advanced logic textbook for a little while; Andy Arana and Gillian Russell are also on the…

We've kept this on the down-low long enough, I think: together with Aldo Antonelli, Jeremy Avigad, Nicole Wyatt, and Audrey Yap, I've been working on an open source advanced logic textbook for a li...

20

4

Add a comment...

### Andrej Bauer

Shared publicly -Suppose we have a triangular mesh in 3D. I would like to "flatten it out" onto a plane, assuming this is possible, for instance because I took a mesh of a torus and cut it along a longitude and a meridian. The mesh is "stretchy" in the sense that we need not preserve the distances between the nodes. What would be a good phisical model for accomplishing this? It does not have to work in all cases, only fairly reasonable ones.

Here's one attempt: put equal electric charges into the vertices of the mesh so that they repel each other, and make all the edges into springs obeying Hook's law (with some natural length). This is not good enough yet, I think.

Here's one attempt: put equal electric charges into the vertices of the mesh so that they repel each other, and make all the edges into springs obeying Hook's law (with some natural length). This is not good enough yet, I think.

2

7 comments

+Andrej Bauer You clearly aren't watching enough of the zombie genre. I feel bad for the people who need to compare their finite element modelling of crash test dummies with ground truth.

Add a comment...

### Andrej Bauer

Shared publicly -Educational math videos can be really helpful, but it takes too long to make them. I spent 3 hours on this one. It answers a question on the hott-cafe mailing list.

#homotopytypetheory

#homotopytypetheory

12

2

8 comments

Mathematica and Keynote, you know, those closed-source commercial apps.

Add a comment...

### Andrej Bauer

Shared publicly -How to make #LaTeX beamer slides with notes, and use #Skim-app to show the notes on your laptop during your talk: https://gist.github.com/andrejbauer/ac361549ac2186be0cdb

- Gist is a simple way to share snippets of text and code with others.

5

3

3 comments

Thanks pdfpc seems useful.

Add a comment...

### Andrej Bauer

Shared publicly -I know about standard references for solving recursive

#domaintheory

**domain**equations. But how about recursive**predomain**equations? One way to deal with them is to take the category of predomains and partial continuous maps which are defined on an open subset, because that category is equivalent to the category of domains, so presumably "things work out". Is there a standard reference for this sort of thing? (It should treat locally continuous functors of mixed variance, preferably on ω-cpos.)#domaintheory

1

Add a comment...

### Andrej Bauer

Shared publicly -I got a letter (excerpt quoted below), and I wonder what the best reply would be. I usually reply, respectfully and to the point. I once found a bug in a two-page proof of Fermat's theorem by a person who wrote math competently but made an honest error involving gcd's. He couldn't get anyone to look at his proof. He thanked me for putting him out of his misery. The present case seems more difficult. Perhaps that video of Vi Hart would help? What do you usually do?

"Respected sir,

Here I am representing different method than others so please go through it. ....[stuff omitted].... The whole world assumes that pi is transcendental number but I want to prove that pi is not transcendental. If you keep this concept apart from your brain & read the whole proof you will also get that assurance. If pi is transcendental then 1 = 0.99999… which is not exact?

.... [stuff omitted] ....Thus I found that the value of π is (17 -8√3)."

"Respected sir,

Here I am representing different method than others so please go through it. ....[stuff omitted].... The whole world assumes that pi is transcendental number but I want to prove that pi is not transcendental. If you keep this concept apart from your brain & read the whole proof you will also get that assurance. If pi is transcendental then 1 = 0.99999… which is not exact?

.... [stuff omitted] ....Thus I found that the value of π is (17 -8√3)."

1

1

31 comments

Andrej Bauer

+

1

2

1

2

1

Well, I do not appreciate such language. I am closing off this discussion because it is a complete waste of time.

### Andrej Bauer

Shared publicly -My student wrote a book on C++!

Our new book is out! Learn about the past, present and future of C++: https://www.jetbrains.com/cpp-today-oreilly/

7

6 comments

Well, Gašper is one of those people who could write a fast program even if he had only clay tables and a toothpick. So I think when he says that C++ code is "readable" you need to understand that correctly. Urs is teasing, but as a teacher I am really proud of Gašper.

Add a comment...

### Andrej Bauer

Shared publicly -It's my pleasure to announce a second PhD position in Ljubljana. It will be surpervised by Alex Simpson, and is in the general area of programming languages and computational effects.

It is my pleasure to announce a second PhD position in Ljubljana! A position is available for a PhD student at the University of Ljubljana in the general research area of modelling and reasoning about computational effects. The precise topic is somewhat flexible, and will be decided in ...

9

1

Add a comment...

### Andrej Bauer

Shared publicly -I am trying to understand why certain math problems are difficult for our freshmen. In the "Logic and sets" course we had the following question, which turns out to be difficult:

They did countable and uncountable sets in our course as well as in the analysis course. We did Cantor's theorem, they know that rationals are countable and reals uncountable, and the midterm had the following question: "Are there two uncountable subsets of the line which intersect in a countably infinite set?"

If anyone wants to perform experiments on their students, I'd love to hear the results.

**"Is there an uncountable family of uncountable subsets of the plane such that any two of them intersect in a countably infinite set?"**They did countable and uncountable sets in our course as well as in the analysis course. We did Cantor's theorem, they know that rationals are countable and reals uncountable, and the midterm had the following question: "Are there two uncountable subsets of the line which intersect in a countably infinite set?"

If anyone wants to perform experiments on their students, I'd love to hear the results.

2

8 comments

As it turns out the problem was not so hard after all. About a quarter of the students solved it. The most common solution was to take a family of straight lines unioned with a fixed countable set (such as the natural numbers as a subset of the line). One solution was to take the graphs x ↦ sin(a x) and another graphs x ↦ sin(x + a), both suitably parametrized by a.

The third problem was in fact harder. It involved proving informally but rigorously the statement:

(∀x,y∈A.φ(x,y)⇔(∃z∈A.ψ(x,z)∧ψ(z,y)) ⇒ (∃u∈A.ψ(u,u))⇒∃v∈A.φ(v,v)).

(It's less complicated than it looks and we did a lot of this systematically.) The second part asked for a counter-example to:

(∀x,y∈A.φ(x,y)⇔(∃z∈A.ψ(x,z)∧ψ(z,y)) ⇒ (∃v∈A.φ(v,v))⇒∃u∈A.ψ(u,u))

I think they got scared by the formulas. But they don't get scared of scary intergrals in the analysis course!

The third problem was in fact harder. It involved proving informally but rigorously the statement:

(∀x,y∈A.φ(x,y)⇔(∃z∈A.ψ(x,z)∧ψ(z,y)) ⇒ (∃u∈A.ψ(u,u))⇒∃v∈A.φ(v,v)).

(It's less complicated than it looks and we did a lot of this systematically.) The second part asked for a counter-example to:

(∀x,y∈A.φ(x,y)⇔(∃z∈A.ψ(x,z)∧ψ(z,y)) ⇒ (∃v∈A.φ(v,v))⇒∃u∈A.ψ(u,u))

I think they got scared by the formulas. But they don't get scared of scary intergrals in the analysis course!

Add a comment...

### Andrej Bauer

Shared publicly -I am looking for a PhD student in the area of homotopy type theory or design of proof assistants.

And did you know Ljubljana is second only to Greece as a top European destination according to Lonely Planet (http://www.lonelyplanet.com/europe/travel-tips-and-articles/lonely-planets-best-in-europe-2014)? It's one of the greenest and most livable cities in Europe.

#HomotopyTypeTheory #scholarship

And did you know Ljubljana is second only to Greece as a top European destination according to Lonely Planet (http://www.lonelyplanet.com/europe/travel-tips-and-articles/lonely-planets-best-in-europe-2014)? It's one of the greenest and most livable cities in Europe.

#HomotopyTypeTheory #scholarship

I am looking for a PhD student in mathematics. Full tuition & stipend will be provided for a period of three years, which is also the official length of the programme. The topic of research is somewhat flexible and varies from constructive models of homotopy type theory to development of a ...

12

6

5 comments

Fixed the year, thanks +Aleš Bizjak .

Add a comment...

### Andrej Bauer

Shared publicly -Thanks to the #TEDx University of Ljubljana team for a great event yesterday. I am releasing the code, the images, and all the animations from my talk, plus some extra animations not shown in the talk. Enjoy!

I spoke about the Beauty of Roots as described by +John Baez on his web page. I calculated the roots of polynomials with coefficients ±1 up to degree 26 and beat the current record by +Sam Derbyshire by 2 degrees. The race is on!

#tedtalk #mathematics

I spoke about the Beauty of Roots as described by +John Baez on his web page. I calculated the roots of polynomials with coefficients ±1 up to degree 26 and beat the current record by +Sam Derbyshire by 2 degrees. The race is on!

#tedtalk #mathematics

12

5

3 comments

Cool, thank you +Andrej Bauer! Now i'm left with the task to find out how i could have come up with your explanation myself. Reason to look at it many more times. Beautiful thing!

Add a comment...

Work

Employment

- University of LjubljanaProfessor, present

Places

Currently

Ljubljana, Slovenia

Previously

Pittsburgh, USA - Duino, Italy

Links

Other profiles

Contributor to

- Random art (current)
- Mathematics and computation (current)
- Videos of lectures and talks (current)
- andrej.com (current)

Story

Tagline

Human.

Education

- United World College of the Adriatic1988 - 1990
- Univerza v Ljubljanimathematics, 1990 - 1994
- Carnegie Mellon Universitylogic, 1994 - 2000

Basic Information

Gender

Male